src/HOL/thy_syntax.ML
changeset 1475 7f5a4cd08209
parent 1465 5d7a7e439cec
child 1574 5a63ab90ee8a
     1.1 --- a/src/HOL/thy_syntax.ML	Mon Feb 05 14:44:09 1996 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Mon Feb 05 21:27:16 1996 +0100
     1.3 @@ -17,9 +17,9 @@
     1.4  open ThyParse;
     1.5  
     1.6  
     1.7 -(** subtype **)
     1.8 +(** typedef **)
     1.9  
    1.10 -fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
    1.11 +fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
    1.12    let
    1.13      val name' = if_none opt_name t;
    1.14      val name = strip_quotes name';
    1.15 @@ -29,10 +29,10 @@
    1.16          "Abs_" ^ name ^ "_inverse"])
    1.17    end;
    1.18  
    1.19 -val subtype_decl =
    1.20 +val typedef_decl =
    1.21    optional ("(" $$-- name --$$ ")" >> Some) None --
    1.22    type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
    1.23 -  >> mk_subtype_decl;
    1.24 +  >> mk_typedef_decl;
    1.25  
    1.26  
    1.27  
    1.28 @@ -191,7 +191,7 @@
    1.29  val user_keywords = ["intrs", "monos", "con_defs", "|"];
    1.30  
    1.31  val user_sections =
    1.32 - [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl,
    1.33 + [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
    1.34    ("inductive", inductive_decl ""),
    1.35    ("coinductive", inductive_decl "Co"),
    1.36    ("datatype", datatype_decl),