# HG changeset patch
# User wenzelm
# Date 962615588 -7200
# Node ID 1f734dc2e526429e0f27ba2b1dadaff5bafd851c
# Parent  0013b2aa98ddc56af2e0681332622f9bceb7c12b
previde 'defs' field for quick_and_dirty;

diff -r 0013b2aa98dd -r 1f734dc2e526 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sat Jul 01 20:01:36 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Jul 03 11:13:08 2000 +0200
@@ -718,7 +718,7 @@
     val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames);
 
     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
-    val (thy', _, _, _, _, _) =
+    val (thy', _, fp_def, rec_sets_defs, _, _) =
       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
         params paramTs cTs cnames;
     val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
@@ -747,7 +747,7 @@
       |>> Theory.parent_path;
     val induct' = if coind then raw_induct else PureThy.get_thm thy''' "induct";
   in (thy''',
-    {defs = [],
+    {defs = fp_def :: rec_sets_defs,
      mono = Drule.asm_rl,
      unfold = Drule.asm_rl,
      intrs = intrs',