src/HOL/Tools/datatype_package.ML
changeset 10525 3e21ab3e5114
parent 10279 b223a9a3350e
child 10911 eb5721204b38
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Nov 27 16:40:56 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Nov 28 01:08:50 2000 +0100
     1.3 @@ -295,7 +295,7 @@
     1.4            (if i + 1 < n then (fn th => th RS conjunct1) else I)
     1.5              (Library.funpow i (fn th => th RS conjunct2) thm)
     1.6            |> Drule.standard
     1.7 -          |> RuleCases.name (RuleCases.get thm);
     1.8 +          |> RuleCases.save thm;
     1.9  
    1.10      fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
    1.11        (("", proj index (length descr) induction), [InductAttrib.induct_type_global name]) ::