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/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
changeset 74381 79f484b0e35b
parent 70494 41108e3e9ca5 
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Sep 28 22:12:52 2021 +0200
@@ -42,7 +42,7 @@
   let
     fun instantiate_with_lambda thm =
       let
-        val prop as \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) =
+        val prop as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>HOL.eq _ for \<open>Var (_, fT) $ _\<close> _\<close>\<close>\<close> =
           Thm.prop_of thm;
         val T = range_type fT;
         val j = Term.maxidx_of_term prop + 1;
isabelle