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/Lifting/lifting_setup.ML
changeset 74545 6c123914883a
parent 74266 612b7e0d6721
child 75503 e5d88927e017 
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Oct 19 14:41:29 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Oct 19 14:58:22 2021 +0200
@@ -148,7 +148,7 @@
         pcr_rel_def
         |> infer_instantiate args_ctxt args_inst
         |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv 
-          (Transfer.bottom_rewr_conv (Transfer.get_relator_eq args_ctxt))))
+          (Conv.bottom_rewrs_conv (Transfer.get_relator_eq args_ctxt) args_ctxt)))
   in
     case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of
       Const (\<^const_name>\<open>relcompp\<close>, _) $ Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ =>
isabelle