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/HOL/Tools/BNF/bnf_lfp_compat.ML
changeset 60728 26ffdb966759
parent 60004 e27e7be1f2f6
child 62324 ae44f16dcea5 
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Jul 16 10:48:20 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Jul 16 12:23:22 2015 +0200
@@ -153,7 +153,7 @@
 
     fun tac ctxt =
       unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN
-      HEADGOAL (rtac refl);
+      HEADGOAL (rtac ctxt refl);
 
     fun prove goal =
       Goal.prove_sorry ctxt [] [] goal (tac o #context)
isabelle