diff -r e66efbafbf1f -r 9c8909fc5865 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Sat Jul 08 12:54:32 2006 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Sat Jul 08 12:54:33 2006 +0200
@@ -259,8 +259,8 @@
     val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
     val _ = message ("Proving equations for primrec function(s) " ^
       commas_quote (map fst nameTs1) ^ " ...");
-    val simps = map (fn (_, t) => standard (Goal.prove thy' [] [] t
-        (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
+    val simps = map (fn (_, t) => Goal.prove_global thy' [] [] t
+        (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
     val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
     val thy''' = thy''
       |> (snd o PureThy.add_thmss [(("simps", simps'),