diff -r 59203adfc33f -r ccda99401bc8 src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Thu Oct 30 22:45:19 2014 +0100
@@ -247,7 +247,8 @@
         val rewrites = rec_rewrites' @ map (snd o snd) defs;
       in
         map (fn eq => Goal.prove ctxt frees [] eq
-          (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, rtac refl 1])) eqs
+          (fn {context = ctxt', ...} =>
+            EVERY [rewrite_goals_tac ctxt' rewrites, resolve_tac [refl] 1])) eqs
       end;
   in ((prefix, (fs, defs)), prove) end
   handle PrimrecError (msg, some_eqn) =>