changeset 59498 | 50b60f501b05 |
parent 58839 | ccda99401bc8 |
child 59859 | f9d1442c70f3 |
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Tue Feb 10 14:29:36 2015 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Tue Feb 10 14:48:26 2015 +0100 @@ -248,7 +248,7 @@ 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) =>