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 70494 41108e3e9ca5
parent 69593 3dda49e08b9d
child 80634 a90ab1ea6458 
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -158,7 +158,7 @@
 
     fun prove goal =
       Goal.prove_sorry ctxt [] [] goal (tac o #context)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
   in
     map (map prove) goalss
   end;
isabelle