--- a/src/HOL/Tools/primrec_package.ML Sat Oct 22 01:22:10 2005 +0200
+++ b/src/HOL/Tools/primrec_package.ML Tue Oct 25 18:18:49 2005 +0200
@@ -254,8 +254,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) => OldGoals.prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
- (fn _ => [rtac refl 1])) eqns;
+ val simps = map (fn (_, t) => standard (Goal.prove thy' [] [] t
+ (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
val thy''' = thy''
|> (#1 o PureThy.add_thmss [(("simps", simps'),