tuned;

--- a/src/HOL/Eisbach/Tests.thy	Sat Apr 10 14:56:03 2021 +0200
+++ b/src/HOL/Eisbach/Tests.thy	Sat Apr 10 19:45:51 2021 +0200
@@ -248,7 +248,7 @@
 
 ML \<open>
   fun test_internal_fact ctxt factnm =
-    (case try (Proof_Context.get_thms ctxt) factnm of
+    (case \<^try>\<open>Proof_Context.get_thms ctxt factnm\<close> of
       NONE => ()
     | SOME _ => error "Found internal fact");
 \<close>

--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Sat Apr 10 14:56:03 2021 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Sat Apr 10 19:45:51 2021 +0200
@@ -17,12 +17,12 @@
 val mk_term_type_internal = Logic.protect o Logic.mk_term o Logic.mk_type;
 
 fun term_type_cases f g t = 
-  (case (try (Logic.dest_type o Logic.dest_term o Logic.unprotect) t) of
+  (case \<^try>\<open>Logic.dest_type (Logic.dest_term (Logic.unprotect t))\<close> of
     SOME T => f T
-  | NONE => 
-    (case (try Logic.dest_term t) of
-      SOME t => g t
-    | NONE => raise Fail "Lost encoded instantiation"))
+  | NONE =>
+      (case \<^try>\<open>Logic.dest_term t\<close> of
+        SOME t => g t
+      | NONE => raise Fail "Lost encoded instantiation"))
 
 fun add_thm_insts ctxt thm =
   let

--- a/src/HOL/Eisbach/match_method.ML	Sat Apr 10 14:56:03 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Sat Apr 10 19:45:51 2021 +0200
@@ -270,7 +270,7 @@
         (fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att))
           | _ => NONE) fact_insts';
 
-    fun try_dest_term thm = try (dest_internal_fact #> snd) thm;
+    fun try_dest_term thm = \<^try>\<open>#2 (dest_internal_fact thm)\<close>;
 
     fun expand_fact fact_insts thm =
       the_default [thm]