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_comp.ML
changeset 63824 24c4fa81f81c
parent 63802 94336cf98486
child 63836 2f9ee7d85d85 
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 08 00:43:21 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 08 10:16:37 2016 +0200
@@ -306,7 +306,7 @@
             (fn {context = ctxt, prems = _} =>
               mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer))
           |> Thm.close_derivation)
-        (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
+        (map2 (curry mk_Trueprop_eq) sets sets_alt);
 
     fun map_cong0_tac ctxt =
       mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer)
isabelle