src/HOL/thy_syntax.ML
changeset 11822 122834177ec1
parent 11804 d69e7acd9380
child 12050 6934c005aec4
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Oct 17 20:24:37 2001 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Oct 17 20:25:19 2001 +0200
     1.3 @@ -280,7 +280,7 @@
     1.4  val _ = ThySyn.add_syntax
     1.5   ["intrs", "monos", "con_defs", "congs", "simpset", "|",
     1.6    "and", "distinct", "inject", "induct"]
     1.7 - [axm_section "typedef" "|> TypedefPackage.add_typedef_no_result" typedef_decl,
     1.8 + [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl,
     1.9    section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
    1.10    section "inductive" 	"" (inductive_decl false),
    1.11    section "coinductive"	"" (inductive_decl true),