src/HOL/thy_syntax.ML

 struct
 
 open ThyParse;
 
 
-(** subtype **)
-
-fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
+(** typedef **)
+
+fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
   let
     val name' = if_none opt_name t;
     val name = strip_quotes name';
   in
     (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
       [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
         "Abs_" ^ name ^ "_inverse"])
   end;
 
-val subtype_decl =
+val typedef_decl =
   optional ("(" $$-- name --$$ ")" >> Some) None --
   type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
-  >> mk_subtype_decl;
+  >> mk_typedef_decl;
 
 
 
 (** (co)inductive **)
 

 (** sections **)
 
 val user_keywords = ["intrs", "monos", "con_defs", "|"];
 
 val user_sections =
- [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl,
+ [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
   ("inductive", inductive_decl ""),
   ("coinductive", inductive_decl "Co"),
   ("datatype", datatype_decl),
   ("primrec", primrec_decl)];