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/Eisbach/match_method.ML
changeset 73553 b35ef8162807
parent 69593 3dda49e08b9d
child 74152 069f6b2c5a07 
--- 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]
isabelle