# HG changeset patch
# User wenzelm
# Date 939388103 -7200
# Node ID 42e94b618f3481e7455303faec9adcf0aa30361f
# Parent  38a46d9ea08aecc58c9d983c4e89956ee9e4e611
return stored thms with proper naming in derivation;

diff -r 38a46d9ea08a -r 42e94b618f34 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Oct 08 15:04:32 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Oct 08 15:08:23 1999 +0200
@@ -677,16 +677,18 @@
       |> (if no_ind then I else PureThy.add_thms
         [((coind_prefix coind ^ "induct", induct), [])])
       |> Theory.parent_path;
-
+    val intrs' = PureThy.get_thms thy'' "intrs";
+    val elims' = PureThy.get_thms thy'' "elims";
+    val induct' = PureThy.get_thm thy'' (coind_prefix coind ^ "induct");
   in (thy'',
     {defs = fp_def::rec_sets_defs,
      mono = mono,
      unfold = unfold,
-     intrs = intrs,
-     elims = elims,
-     mk_cases = mk_cases elims,
+     intrs = intrs',
+     elims = elims',
+     mk_cases = mk_cases elims',
      raw_induct = raw_induct,
-     induct = induct})
+     induct = induct'})
   end;
 
 
@@ -725,6 +727,7 @@
       |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
       |> Theory.parent_path;
+    val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
   in (thy'',
     {defs = [],
      mono = TrueI,
@@ -733,7 +736,7 @@
      elims = elims,
      mk_cases = mk_cases elims,
      raw_induct = raw_induct,
-     induct = induct})
+     induct = induct'})
   end;
 
 
diff -r 38a46d9ea08a -r 42e94b618f34 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Fri Oct 08 15:04:32 1999 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Oct 08 15:08:23 1999 +0200
@@ -84,17 +84,22 @@
     val _ = message ("Defining recursive function " ^ quote name ^ " ...");
 
     val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
-    val (thy1, congs) = thy |> app_thms raw_congs;
-    val (thy2, result as {rules, induct, tcs}) = 
-        tfl_fn thy1 name R (ss, congs) eqs
-    val thy3 =
-      thy2
+    val (thy, congs) = thy |> app_thms raw_congs;
+    val (thy, {rules, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
+    val thy =
+      thy
       |> Theory.add_path bname
       |> PureThy.add_thmss [(("rules", rules), [])]
-      |> PureThy.add_thms [(("induct", induct), [])]
+      |> PureThy.add_thms [(("induct", induct), [])];
+    val result =
+     {rules = PureThy.get_thms thy "rules",
+      induct = PureThy.get_thm thy "induct",
+      tcs = tcs};
+    val thy =
+      thy
       |> put_recdef name result
       |> Theory.parent_path;
-  in (thy3, result) end;
+  in (thy, result) end;
 
 val add_recdef = gen_add_recdef Tfl.define I IsarThy.apply_theorems;
 val add_recdef_x = gen_add_recdef Tfl.define (Simplifier.simpset_of o ThyInfo.get_theory)