src/HOL/Analysis/measurable.ML

--- a/src/HOL/Analysis/measurable.ML	Fri Apr 09 22:06:59 2021 +0200
+++ b/src/HOL/Analysis/measurable.ML	Sat Apr 10 14:55:50 2021 +0200
@@ -274,7 +274,7 @@
     val t = HOLogic.mk_Trueprop (Thm.term_of redex);
     fun tac {context = ctxt, prems = _ } =
       SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt));
-  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
+  in \<^try>\<open>Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}\<close> end;
 
 end