Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
RuleCases.save;
authorwenzelm
Tue, 28 Nov 2000 01:08:50 +0100
changeset 10525 3e21ab3e5114
parent 10524 270b285d48ee
child 10526 ced4f4ec917e
RuleCases.save;
src/HOL/Tools/datatype_package.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/primrec_package.ML file | annotate | diff | comparison | revisions 
--- 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]) ::
--- 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 =
isabelle