src/HOL/Tools/Old_Datatype/old_primrec.ML

         val frees = fold (Variable.add_free_names ctxt) eqs [];
         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, resolve_tac [refl] 1])) eqs
+            EVERY [rewrite_goals_tac ctxt' rewrites, resolve_tac ctxt' [refl] 1])) eqs
       end;
   in ((prefix, (fs, defs)), prove) end
   handle PrimrecError (msg, some_eqn) =>
     error ("Primrec definition error:\n" ^ msg ^
       (case some_eqn of