# HG changeset patch
# User wenzelm
# Date 859891452 -7200
# Node ID b6a5780e36b922d361c91849c4d3867ece61edc2
# Parent  a66196e1668c7fdd3cab046c4a2bb963c6ec74fc
improved messages;

diff -r a66196e1668c -r b6a5780e36b9 src/HOL/typedef.ML
--- a/src/HOL/typedef.ML	Tue Apr 01 11:16:06 1997 +0200
+++ b/src/HOL/typedef.ML	Tue Apr 01 12:44:12 1997 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Internal interface for typedef definitions.
+Internal interface for typedefs.
 *)
 
 signature TYPEDEF =
@@ -45,7 +45,7 @@
 
 fun ext_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
   let
-    val dummy = require_thy thy "Set" "typedef definitions";
+    val dummy = require_thy thy "Set" "typedefs";
     val sign = sign_of thy;
 
     (*rhs*)
@@ -122,7 +122,7 @@
       (Abs_name ^ "_inverse", abs_type_inv)]
   end
   handle ERROR =>
-    error ("The error(s) above occurred in typedef definition " ^ quote name);
+    error ("The error(s) above occurred in typedef " ^ quote name);
 
 
 (* external interfaces *)
@@ -138,4 +138,3 @@
 
 
 end;
-