src/HOL/Tools/inductive_package.ML
changeset 7798 42e94b618f34
parent 7710 bf8cb3fc5d64
child 8100 6186ee807f2e
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Oct 08 15:04:32 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Oct 08 15:08:23 1999 +0200
     1.3 @@ -677,16 +677,18 @@
     1.4        |> (if no_ind then I else PureThy.add_thms
     1.5          [((coind_prefix coind ^ "induct", induct), [])])
     1.6        |> Theory.parent_path;
     1.7 -
     1.8 +    val intrs' = PureThy.get_thms thy'' "intrs";
     1.9 +    val elims' = PureThy.get_thms thy'' "elims";
    1.10 +    val induct' = PureThy.get_thm thy'' (coind_prefix coind ^ "induct");
    1.11    in (thy'',
    1.12      {defs = fp_def::rec_sets_defs,
    1.13       mono = mono,
    1.14       unfold = unfold,
    1.15 -     intrs = intrs,
    1.16 -     elims = elims,
    1.17 -     mk_cases = mk_cases elims,
    1.18 +     intrs = intrs',
    1.19 +     elims = elims',
    1.20 +     mk_cases = mk_cases elims',
    1.21       raw_induct = raw_induct,
    1.22 -     induct = induct})
    1.23 +     induct = induct'})
    1.24    end;
    1.25  
    1.26  
    1.27 @@ -725,6 +727,7 @@
    1.28        |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
    1.29        |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
    1.30        |> Theory.parent_path;
    1.31 +    val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
    1.32    in (thy'',
    1.33      {defs = [],
    1.34       mono = TrueI,
    1.35 @@ -733,7 +736,7 @@
    1.36       elims = elims,
    1.37       mk_cases = mk_cases elims,
    1.38       raw_induct = raw_induct,
    1.39 -     induct = induct})
    1.40 +     induct = induct'})
    1.41    end;
    1.42  
    1.43