src/HOL/typedef.ML

 (*  Title:      HOL/typedef.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Internal interface for typedef definitions.
+Internal interface for typedefs.
 *)
 
 signature TYPEDEF =
 sig
   val prove_nonempty: cterm -> thm list -> tactic option -> thm

 
 (* ext_typedef *)
 
 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*)
     val cset = prep_term sign raw_set;
     val {T = setT, t = set, ...} = rep_cterm cset;

      [(Rep_name, rep_type),
       (Rep_name ^ "_inverse", rep_type_inv),
       (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 *)
 
 fun cert_term sg tm =

 val add_typedef = ext_typedef read_term;
 val add_typedef_i = ext_typedef cert_term;
 
 
 end;
-