--- 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',