Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Tools/primrec_package.ML
changeset 59498 50b60f501b05
parent 58838 59203adfc33f
child 59582 0fbed69ff081 
--- a/src/ZF/Tools/primrec_package.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -177,7 +177,7 @@
       eqn_terms |> map (fn t =>
         Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
           (fn {context = ctxt, ...} =>
-            EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac @{thms refl} 1]));
+            EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac ctxt @{thms refl} 1]));
 
     val (eqn_thms', thy2) =
       thy1
isabelle