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_term.ML
changeset 81954 6f2bcdfa9a19
parent 80675 e9beaa28645d 
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -463,7 +463,7 @@
             | _ => false
   
           val inst_distr_rule = rewr_imp distr_rule ctm
-          val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule)
+          val extra_assms = filter_out is_POS_or_NEG (Thm.cprems_of inst_distr_rule)
           val proved_assms = map_interrupt prove_assm extra_assms
         in
           Option.map (curry op OF inst_distr_rule) proved_assms
@@ -491,7 +491,7 @@
                   case distr_rule of
                     NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ())
                   | SOME distr_rule =>
-                      map (gen_merge_transfer_relations quotients ctxt0) (cprems_of distr_rule)
+                      map (gen_merge_transfer_relations quotients ctxt0) (Thm.cprems_of distr_rule)
                         MRSL distr_rule
                 end
               else
@@ -504,7 +504,7 @@
                       val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
                       val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
                       val result = (map (gen_merge_transfer_relations quotients ctxt0) 
-                        (cprems_of distr_rule)) MRSL distr_rule
+                        (Thm.cprems_of distr_rule)) MRSL distr_rule
                       val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def)
                     in  
                       Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv
isabelle