# HG changeset patch
# User wenzelm
# Date 975370130 -3600
# Node ID 3e21ab3e5114747236a42f4a4f161f0d78027ac6
# Parent  270b285d48ee48f3c9d921355f222530fb880cc6
RuleCases.save;

diff -r 270b285d48ee -r 3e21ab3e5114 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Nov 27 16:40:56 2000 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Nov 28 01:08:50 2000 +0100
@@ -295,7 +295,7 @@
           (if i + 1 < n then (fn th => th RS conjunct1) else I)
             (Library.funpow i (fn th => th RS conjunct2) thm)
           |> Drule.standard
-          |> RuleCases.name (RuleCases.get thm);
+          |> RuleCases.save thm;
 
     fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
       (("", proj index (length descr) induction), [InductAttrib.induct_type_global name]) ::
diff -r 270b285d48ee -r 3e21ab3e5114 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Mon Nov 27 16:40:56 2000 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Tue Nov 28 01:08:50 2000 +0100
@@ -266,7 +266,7 @@
   in
     induction
     |> RuleCases.rename_params (map params_of (flat (map (map #1 o #3 o #2) descr)))
-    |> RuleCases.name (RuleCases.get induction)
+    |> RuleCases.save induction
   end;
 
 fun add_primrec_i alt_name eqns_atts thy =