--- a/src/HOL/Tools/Meson/meson.ML Fri Apr 09 22:06:59 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Sat Apr 10 14:55:50 2021 +0200
@@ -97,7 +97,7 @@
(*FIXME: currently does not "rename variables apart"*)
fun first_order_resolve ctxt thA thB =
(case
- try (fn () =>
+ \<^try>\<open>
let val thy = Proof_Context.theory_of ctxt
val tmA = Thm.concl_of thA
val Const(\<^const_name>\<open>Pure.imp\<close>,_) $ tmB $ _ = Thm.prop_of thB
@@ -105,7 +105,7 @@
Pattern.first_order_match thy (tmB, tmA)
(Vartab.empty, Vartab.empty) |> snd
val insts = Vartab.fold (fn (xi, (_, t)) => cons (xi, Thm.cterm_of ctxt t)) tenv [];
- in thA RS (infer_instantiate ctxt insts thB) end) () of
+ in thA RS (infer_instantiate ctxt insts thB) end\<close> of
SOME th => th
| NONE => raise THM ("first_order_resolve", 0, [thA, thB]))