src/HOL/Library/Countable.thy

--- a/src/HOL/Library/Countable.thy	Fri Apr 09 21:07:11 2021 +0200
+++ b/src/HOL/Library/Countable.thy	Fri Apr 09 22:06:59 2021 +0200
@@ -204,7 +204,7 @@
 
 ML \<open>
 fun countable_datatype_tac ctxt st =
-  (case try (fn () => HEADGOAL (old_countable_datatype_tac ctxt) st) () of
+  (case \<^try>\<open>HEADGOAL (old_countable_datatype_tac ctxt) st\<close> of
     SOME res => res
   | NONE => BNF_LFP_Countable.countable_datatype_tac ctxt st);