equal
deleted
inserted
replaced
872 in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end; |
872 in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end; |
873 |
873 |
874 fun rewrite_eqn thy conv ss = |
874 fun rewrite_eqn thy conv ss = |
875 let |
875 let |
876 val ctxt = Proof_Context.init_global thy; |
876 val ctxt = Proof_Context.init_global thy; |
877 val rewrite = Conv.fconv_rule (conv (Simplifier.rewrite ss)); |
877 val rewrite = Conv.fconv_rule (conv (Simplifier.rewrite (put_simpset ss ctxt))); |
878 in singleton (Variable.trade (K (map rewrite)) ctxt) end; |
878 in singleton (Variable.trade (K (map rewrite)) ctxt) end; |
879 |
879 |
880 fun cert_of_eqns_preprocess thy functrans ss c = |
880 fun cert_of_eqns_preprocess thy functrans ss c = |
881 (map o apfst) (Thm.transfer thy) |
881 (map o apfst) (Thm.transfer thy) |
882 #> perhaps (perhaps_loop (perhaps_apply functrans)) |
882 #> perhaps (perhaps_loop (perhaps_apply functrans)) |