src/HOL/Tools/inductive_package.ML
changeset 9235 1f734dc2e526
parent 9201 435fef035d7f
child 9298 7d9b562a750b
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Jul 01 20:01:36 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Jul 03 11:13:08 2000 +0200
     1.3 @@ -718,7 +718,7 @@
     1.4      val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames);
     1.5  
     1.6      val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
     1.7 -    val (thy', _, _, _, _, _) =
     1.8 +    val (thy', _, fp_def, rec_sets_defs, _, _) =
     1.9        mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
    1.10          params paramTs cTs cnames;
    1.11      val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
    1.12 @@ -747,7 +747,7 @@
    1.13        |>> Theory.parent_path;
    1.14      val induct' = if coind then raw_induct else PureThy.get_thm thy''' "induct";
    1.15    in (thy''',
    1.16 -    {defs = [],
    1.17 +    {defs = fp_def :: rec_sets_defs,
    1.18       mono = Drule.asm_rl,
    1.19       unfold = Drule.asm_rl,
    1.20       intrs = intrs',