src/HOL/thy_syntax.ML
changeset 11804 d69e7acd9380
parent 11628 e57a6e51715e
child 11822 122834177ec1
     1.1 --- a/src/HOL/thy_syntax.ML	Tue Oct 16 17:51:50 2001 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Tue Oct 16 17:52:07 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" typedef_decl,
     1.8 + [axm_section "typedef" "|> TypedefPackage.add_typedef_no_result" 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),