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/Qelim/cooper.ML
changeset 73550 2f6855142a8c
parent 71937 92de7d74b8f8
child 74282 c2ee8d993d6a 
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Apr 09 21:07:11 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Apr 09 22:06:59 2021 +0200
@@ -739,8 +739,7 @@
     in
       if ntac then no_tac
       else
-        (case try (fn () =>
-            Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
+        (case \<^try>\<open>Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))\<close> of
           NONE => no_tac
         | SOME r => resolve_tac ctxt [r] i)
     end)
isabelle