--- 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]) ::