src/HOL/thy_syntax.ML
changeset 6523 c84935821ba0
parent 6497 120ca2bb27e1
child 6555 17b7b88a8e3c
     1.1 --- a/src/HOL/thy_syntax.ML	Tue Apr 27 10:50:50 1999 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Tue Apr 27 10:51:16 1999 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4          \local\n\
     1.5          \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
     1.6          \  InductivePackage.add_inductive true " ^
     1.7 -        (if coind then "true " else "false ") ^ srec_tms ^ " " ^
     1.8 +        (if coind then "true " else "false ") ^ srec_tms ^ " [] " ^
     1.9           sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
    1.10          \in\n\
    1.11          \structure " ^ big_rec_name ^ " =\n\
    1.12 @@ -280,7 +280,7 @@
    1.13   ["intrs", "monos", "con_defs", "congs", "simpset", "|",
    1.14    "and", "distinct", "inject", "induct", "??"]
    1.15   [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
    1.16 -  section "record" "|> RecordPackage.add_record" record_decl,
    1.17 +  section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
    1.18    section "inductive" 	"" (inductive_decl false),
    1.19    section "coinductive"	"" (inductive_decl true),
    1.20    section "datatype" 	"" datatype_decl,