# HG changeset patch
# User wenzelm
# Date 925203076 -7200
# Node ID c84935821ba04ff821fb8e61e771479f299a21dd
# Parent  2f6cec5c046fba4638a59a03d3c1679c27b52040
adapted add_inductive, add_record;

diff -r 2f6cec5c046f -r c84935821ba0 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Tue Apr 27 10:50:50 1999 +0200
+++ b/src/HOL/thy_syntax.ML	Tue Apr 27 10:51:16 1999 +0200
@@ -55,7 +55,7 @@
         \local\n\
         \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
         \  InductivePackage.add_inductive true " ^
-        (if coind then "true " else "false ") ^ srec_tms ^ " " ^
+        (if coind then "true " else "false ") ^ srec_tms ^ " [] " ^
          sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
         \in\n\
         \structure " ^ big_rec_name ^ " =\n\
@@ -280,7 +280,7 @@
  ["intrs", "monos", "con_defs", "congs", "simpset", "|",
   "and", "distinct", "inject", "induct", "??"]
  [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
-  section "record" "|> RecordPackage.add_record" record_decl,
+  section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
   section "inductive" 	"" (inductive_decl false),
   section "coinductive"	"" (inductive_decl true),
   section "datatype" 	"" datatype_decl,