return stored thms with proper naming in derivation;
authorwenzelm
Fri Oct 08 15:08:23 1999 +0200 (1999-10-08)
changeset 779842e94b618f34
parent 7797 38a46d9ea08a
child 7799 4c69318e6a6d
return stored thms with proper naming in derivation;
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/recdef_package.ML
     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  
     2.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Oct 08 15:04:32 1999 +0200
     2.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Oct 08 15:08:23 1999 +0200
     2.3 @@ -84,17 +84,22 @@
     2.4      val _ = message ("Defining recursive function " ^ quote name ^ " ...");
     2.5  
     2.6      val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
     2.7 -    val (thy1, congs) = thy |> app_thms raw_congs;
     2.8 -    val (thy2, result as {rules, induct, tcs}) = 
     2.9 -        tfl_fn thy1 name R (ss, congs) eqs
    2.10 -    val thy3 =
    2.11 -      thy2
    2.12 +    val (thy, congs) = thy |> app_thms raw_congs;
    2.13 +    val (thy, {rules, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
    2.14 +    val thy =
    2.15 +      thy
    2.16        |> Theory.add_path bname
    2.17        |> PureThy.add_thmss [(("rules", rules), [])]
    2.18 -      |> PureThy.add_thms [(("induct", induct), [])]
    2.19 +      |> PureThy.add_thms [(("induct", induct), [])];
    2.20 +    val result =
    2.21 +     {rules = PureThy.get_thms thy "rules",
    2.22 +      induct = PureThy.get_thm thy "induct",
    2.23 +      tcs = tcs};
    2.24 +    val thy =
    2.25 +      thy
    2.26        |> put_recdef name result
    2.27        |> Theory.parent_path;
    2.28 -  in (thy3, result) end;
    2.29 +  in (thy, result) end;
    2.30  
    2.31  val add_recdef = gen_add_recdef Tfl.define I IsarThy.apply_theorems;
    2.32  val add_recdef_x = gen_add_recdef Tfl.define (Simplifier.simpset_of o ThyInfo.get_theory)