--- 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) =>