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_comp.ML
changeset 60757 c09598a97436
parent 60752 b48830b670a1
child 61242 1f92b0ac9c96 
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -247,7 +247,7 @@
           val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
           val goal = mk_Trueprop_mem (bd_bd', ordIso);
         in
-          (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
+          (bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context)
             |> Thm.close_derivation))
         end
       else
isabelle