# HG changeset patch
# User berghofe
# Date 965912121 -7200
# Node ID af71f5f4ca6b433dcd05bd0547087a07dfc38cdd
# Parent  da0a964aa601e6460d8a3ef65a38409b51f99aa2
Equations that are added to the simpset now have proper names.

diff -r da0a964aa601 -r af71f5f4ca6b src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Thu Aug 10 11:39:53 2000 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Thu Aug 10 14:55:21 2000 +0200
@@ -303,14 +303,14 @@
     val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ...");
     val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
         (fn _ => [rtac refl 1])) eqns;
-    val (thy'', [simps']) = thy'
-      |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
-      |>> (#1 o PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts))
-      |>> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
-      |>> Theory.parent_path
+    val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
+    val thy''' = thy''
+      |> (#1 o PureThy.add_thmss [(("simps", simps'), [Simplifier.simp_add_global])])
+      |> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
+      |> Theory.parent_path
   in
     (foldl (fn (thy, (fname, _, _, tname)) =>
-       put_primrec fname (tname, simps') thy) (thy'', defs), simps')
+       put_primrec fname (tname, simps') thy) (thy''', defs), simps')
   end;