--- a/src/FOL/simpdata.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/FOL/simpdata.ML Wed May 21 10:30:34 2025 +0200
@@ -82,7 +82,7 @@
val ex_comm = @{thm ex_comm}
val atomize =
let val rules = @{thms atomize_all atomize_imp atomize_eq atomize_iff atomize_conj}
- in fn ctxt => Raw_Simplifier.rewrite_wrt ctxt true rules end
+ in fn ctxt => Simplifier.rewrite_wrt ctxt true rules end
);
--- a/src/HOL/Library/conditional_parametricity.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML Wed May 21 10:30:34 2025 +0200
@@ -358,7 +358,7 @@
val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
val prop2 = Logic.list_rename_params (rev names) prop1
val cprop = Thm.cterm_of ctxt prop2
- val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false [Domainp_lemma] cprop
+ val equal_thm = Simplifier.rewrite_wrt ctxt false [Domainp_lemma] cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
in
forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -412,7 +412,7 @@
val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
val cprop = Thm.cterm_of ctxt prop2
- val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false [is_equality_lemma] cprop
+ val equal_thm = Simplifier.rewrite_wrt ctxt false [is_equality_lemma] cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
in
forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
--- a/src/HOL/Library/old_recdef.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Library/old_recdef.ML Wed May 21 10:30:34 2025 +0200
@@ -1230,7 +1230,7 @@
rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
fun rew_conv ctxt ctm =
- Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
+ Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
(Variable.declare_term (Thm.term_of ctm) ctxt) ctm;
fun simpl_conv ctxt thl ctm =
@@ -1467,7 +1467,7 @@
val eq = Logic.strip_imp_concl imp
val lhs = tych(get_lhs eq)
val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
- val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
+ val lhs_eq_lhs1 = Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
handle Utils.ERR _ => Thm.reflexive lhs
val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
@@ -1488,7 +1488,7 @@
val QeqQ1 = pbeta_reduce (tych Q)
val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
- val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1
+ val Q1eeqQ2 = Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1
handle Utils.ERR _ => Thm.reflexive Q1
val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
@@ -1513,7 +1513,7 @@
let val tych = Thm.cterm_of ctxt
val ants1 = map tych ants
val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
- val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
+ val Q_eeq_Q1 = Simplifier.rewrite_cterm
(false,true,false) (prover used') ctxt' (tych Q)
handle Utils.ERR _ => Thm.reflexive (tych Q)
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
@@ -1581,7 +1581,7 @@
val ctm = Thm.cprop_of th
val names = Misc_Legacy.add_term_names (Thm.term_of ctm, [])
val th1 =
- Raw_Simplifier.rewrite_cterm (false, true, false)
+ Simplifier.rewrite_cterm (false, true, false)
(prover names) (ctxt0 addsimps [cut_lemma'] |> fold Simplifier.add_eqcong congs) ctm
val th2 = Thm.equal_elim th1 th
in
--- a/src/HOL/Nominal/nominal_inductive.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed May 21 10:30:34 2025 +0200
@@ -18,10 +18,10 @@
val inductive_atomize = @{thms induct_atomize};
val inductive_rulify = @{thms induct_rulify};
-fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
+fun rulify_term thy = Simplifier.rewrite_term thy inductive_rulify [];
fun atomize_conv ctxt =
- Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
+ Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
(put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed May 21 10:30:34 2025 +0200
@@ -19,10 +19,10 @@
val inductive_atomize = @{thms induct_atomize};
val inductive_rulify = @{thms induct_rulify};
-fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
+fun rulify_term thy = Simplifier.rewrite_term thy inductive_rulify [];
fun atomize_conv ctxt =
- Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
+ Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
(put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
--- a/src/HOL/Nonstandard_Analysis/transfer_principle.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Nonstandard_Analysis/transfer_principle.ML Wed May 21 10:30:34 2025 +0200
@@ -74,7 +74,7 @@
val meta = Local_Defs.meta_rewrite_rule ctxt;
val ths' = map meta ths;
val unfolds' = map meta unfolds and refolds' = map meta refolds;
- val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite_wrt ctxt true unfolds' (Thm.cterm_of ctxt t))
+ val (_$_$t') = Thm.concl_of (Simplifier.rewrite_wrt ctxt true unfolds' (Thm.cterm_of ctxt t))
val u = unstar_term consts t'
val tac =
rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed May 21 10:30:34 2025 +0200
@@ -652,7 +652,7 @@
asm_full_simp_tac
(Simplifier.add_simp
@{lemma "(A & B) & C == A & B & C" by auto} (*FIXME duplicates @{thm simp_meta(3)}*)
- (Raw_Simplifier.empty_simpset ctxt))
+ (Simplifier.empty_simpset ctxt))
#> CHANGED
#> REPEAT_DETERM
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed May 21 10:30:34 2025 +0200
@@ -1369,7 +1369,7 @@
rel_inject
|> Thm.instantiate' cTs cts
|> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
- (Raw_Simplifier.rewrite_wrt lthy false
+ (Simplifier.rewrite_wrt lthy false
@{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
|> unfold_thms lthy eq_onps
|> postproc
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed May 21 10:30:34 2025 +0200
@@ -519,7 +519,7 @@
in
@{thm asm_rl[of "\<forall>x. P x \<longrightarrow> Q x" for P Q]}
|> Thm.instantiate' [SOME (Thm.ctyp_of \<^context> T)] []
- |> Raw_Simplifier.rewrite_goals_rule \<^context> @{thms split_paired_All[THEN eq_reflection]}
+ |> Simplifier.rewrite_goals_rule \<^context> @{thms split_paired_All[THEN eq_reflection]}
|> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
|> Thm.varifyT_global
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Wed May 21 10:30:34 2025 +0200
@@ -527,7 +527,7 @@
end);
val phi =
- Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy)
+ Morphism.term_morphism "BNF" (Simplifier.rewrite_term (Proof_Context.theory_of lthy)
@{thms BNF_Composition.id_bnf_def} [])
$> Morphism.thm_morphism "BNF" (unfold_thms lthy @{thms BNF_Composition.id_bnf_def});
in
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed May 21 10:30:34 2025 +0200
@@ -83,8 +83,8 @@
fun unfold_id_bnf_etc lthy =
let val thy = Proof_Context.theory_of lthy in
- Raw_Simplifier.rewrite_term thy unfold_id_thms1 []
- #> Raw_Simplifier.rewrite_term thy @{thms BNF_Composition.id_bnf_def} []
+ Simplifier.rewrite_term thy unfold_id_thms1 []
+ #> Simplifier.rewrite_term thy @{thms BNF_Composition.id_bnf_def} []
end;
datatype corec_option =
@@ -242,7 +242,7 @@
val goal = mk_Trueprop_eq (list_comb (casex, fs) $ u,
mk_case_absumprod absT rep fs xss xss $ u')
- |> Raw_Simplifier.rewrite_term thy @{thms comp_def[THEN eq_reflection]} [];
+ |> Simplifier.rewrite_term thy @{thms comp_def[THEN eq_reflection]} [];
val vars = map (fst o dest_Free) (u :: fs);
val dtor_ctor = nth dtor_ctors fp_res_index;
@@ -553,7 +553,7 @@
unfold_thms_tac ctxt simps THEN HEADGOAL (rtac ctxt rho_transfer')))
|> Thm.close_derivation \<^here>;
- val goal' = Raw_Simplifier.rewrite_term thy simps [] goal;
+ val goal' = Simplifier.rewrite_term thy simps [] goal;
in
if null abs_rep_transfers then (goal', derive_unprimed #> fold_rho)
else (goal, fold_rho)
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Wed May 21 10:30:34 2025 +0200
@@ -133,7 +133,7 @@
val simp_ctxt = (ctxt
|> Context_Position.set_visible false
|> put_simpset (simpset_of (Proof_Context.init_global \<^theory>\<open>Main\<close>))
- |> Raw_Simplifier.add_cong @{thm if_cong})
+ |> Simplifier.add_cong @{thm if_cong})
addsimps pre_map_def :: abs_inverse :: fp_map_ident :: dtor_ctor :: rho_def ::
@{thm convol_def} :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @
fpsig_nesting_map_thms @ live_nesting_map_ident0s @ ctr_defs @ disc_sel_eq_cases' @
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed May 21 10:30:34 2025 +0200
@@ -79,7 +79,7 @@
etac ctxt disjE))));
fun ss_fst_snd_conv ctxt =
- Raw_Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
+ Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
fun case_atac ctxt =
Simplifier.full_simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
--- a/src/HOL/Tools/Function/induction_schema.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Wed May 21 10:30:34 2025 +0200
@@ -37,12 +37,12 @@
branches: scheme_branch list,
cases: scheme_case list}
-fun ind_atomize ctxt = Raw_Simplifier.rewrite_wrt ctxt true @{thms induct_atomize}
-fun ind_rulify ctxt = Raw_Simplifier.rewrite_wrt ctxt true @{thms induct_rulify}
+fun ind_atomize ctxt = Simplifier.rewrite_wrt ctxt true @{thms induct_atomize}
+fun ind_rulify ctxt = Simplifier.rewrite_wrt ctxt true @{thms induct_rulify}
fun meta thm = thm RS eq_reflection
-fun sum_prod_conv ctxt = Raw_Simplifier.rewrite_wrt ctxt true
+fun sum_prod_conv ctxt = Simplifier.rewrite_wrt ctxt true
(map meta (@{thm split_conv} :: @{thms sum.case}))
fun term_conv ctxt cv t =
--- a/src/HOL/Tools/Function/partial_function.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Wed May 21 10:30:34 2025 +0200
@@ -178,7 +178,7 @@
THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
|> (fn thm => thm OF [mono_thm, f_def])
|> Conv.fconv_rule (Conv.concl_conv ~1 (* simplify conclusion *)
- (Raw_Simplifier.rewrite_wrt ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
+ (Simplifier.rewrite_wrt ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
|> singleton (Variable.export ctxt' ctxt)
end
--- a/src/HOL/Tools/Lifting/lifting_def.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed May 21 10:30:34 2025 +0200
@@ -196,7 +196,7 @@
Conv.fconv_rule
((Conv.concl_conv (Thm.nprems_of inst_thm) o
HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
- (Raw_Simplifier.rewrite_wrt ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
+ (Simplifier.rewrite_wrt ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
end
fun inst_relcomppI ctxt ant1 ant2 =
@@ -629,7 +629,7 @@
val rty_forced = (domain_type o fastype_of) rsp_rel;
val forced_rhs = force_rty_type ctxt rty_forced rhs;
val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv
- (Raw_Simplifier.rewrite_wrt ctxt false (get_cr_pcr_eqs ctxt)))
+ (Simplifier.rewrite_wrt ctxt false (get_cr_pcr_eqs ctxt)))
val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
|> Thm.cterm_of ctxt
|> cr_to_pcr_conv
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed May 21 10:30:34 2025 +0200
@@ -418,7 +418,7 @@
rtac ctxt unfold_lift_sel_rsp THEN'
case_tac exhaust_rule ctxt THEN_ALL_NEW (
EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *)
- Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules),
+ Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules),
REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])) i
val pred_simps = Transfer.lookup_pred_data lthy5 (Tname rty) |> the |> Transfer.pred_simps
val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps)
@@ -439,7 +439,7 @@
EVERY' [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms type_definition_def}),
DETERM o Transfer.transfer_tac true ctxt,
SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms eq_onp_top_eq_eq}) (* normalize *),
- Raw_Simplifier.rewrite_goal_tac ctxt
+ Simplifier.rewrite_goal_tac ctxt
(map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
rtac ctxt TrueI] i;
@@ -515,7 +515,7 @@
in
EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o (Transfer.transfer_tac true ctxt),
case_tac exhaust ctxt THEN_ALL_NEW EVERY' [hyp_subst_tac ctxt,
- Raw_Simplifier.rewrite_goal_tac ctxt simp_rules, rtac ctxt TrueI ]] i
+ Simplifier.rewrite_goal_tac ctxt simp_rules, rtac ctxt TrueI ]] i
end
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed May 21 10:30:34 2025 +0200
@@ -955,7 +955,7 @@
val Tcon = datatype_name_of_case_name thy case_name
val th = instantiated_case_rewrite thy Tcon
in
- Raw_Simplifier.rewrite_term thy [th RS @{thm eq_reflection}] [] t
+ Simplifier.rewrite_term thy [th RS @{thm eq_reflection}] [] t
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed May 21 10:30:34 2025 +0200
@@ -97,7 +97,7 @@
(Const (\<^const_name>\<open>If\<close>, _)) =>
let
val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
- val atom' = Raw_Simplifier.rewrite_term thy
+ val atom' = Simplifier.rewrite_term thy
(map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
val _ = \<^assert> (not (atom = atom'))
in
--- a/src/HOL/Tools/SMT/cvc5_replay.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/cvc5_replay.ML Wed May 21 10:30:34 2025 +0200
@@ -40,14 +40,14 @@
(Lethe_Proof.Lethe_Replay_Node {id, rule, concl, bounds, declarations = decls, ...}) =
let
val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy rewrite_rules []
+ Simplifier.rewrite_term thy rewrite_rules []
#> not (null ll_defs andalso Lethe_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
end
val rewrite_concl = if Lethe_Proof.keep_app_symbols rule then
filter (curry Term.could_unify (Thm.concl_of @{thm SMT.fun_app_def}) o Thm.concl_of) rewrite_rules
else rewrite_rules
val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy rewrite_concl []
+ Simplifier.rewrite_term thy rewrite_concl []
#> Object_Logic.atomize_term ctxt
#> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
#> SMTLIB_Isar.unskolemize_names ctxt
@@ -112,7 +112,7 @@
(ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes))))
val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy ((if Lethe_Proof.keep_raw_lifting rule andalso not (null rewrite_rules) then tl rewrite_rules else rewrite_rules)) []
+ Simplifier.rewrite_term thy ((if Lethe_Proof.keep_raw_lifting rule andalso not (null rewrite_rules) then tl rewrite_rules else rewrite_rules)) []
#> Object_Logic.atomize_term ctxt
#> not (null ll_defs andalso Lethe_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
#> SMTLIB_Isar.unskolemize_names ctxt
@@ -180,7 +180,7 @@
val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state
val global_transformer = subst_only_free global_transformation
val rewrite = let val thy = Proof_Context.theory_of ctxt in
- Raw_Simplifier.rewrite_term thy (rewrite_rules) []
+ Simplifier.rewrite_term thy (rewrite_rules) []
#> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
end
val start0 = Timing.start ()
@@ -216,7 +216,7 @@
fun replay_assumed assms ll_defs rewrite_rules stats ctxt term =
let
val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy rewrite_rules []
+ Simplifier.rewrite_term thy rewrite_rules []
#> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
end
val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term))
@@ -299,7 +299,7 @@
prems = [],
proof_ctxt = [],
concl = Thm.prop_of th'
- |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
+ |> Simplifier.rewrite_term (Proof_Context.theory_of
(empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [],
bounds = [],
insts = Symtab.empty,
@@ -310,7 +310,7 @@
val used_assert_ids = fold add_used_asserts_in_step actual_steps []
fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy rewrite_rules [] end
+ Simplifier.rewrite_term thy rewrite_rules [] end
val used_assm_js =
map_filter (fn (id, th) => let val i = index_of_id id in if i >= 0 then SOME (i, th)
else NONE end)
--- a/src/HOL/Tools/SMT/cvc_proof_parse.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/cvc_proof_parse.ML Wed May 21 10:30:34 2025 +0200
@@ -38,7 +38,7 @@
#> Thm.eta_long_conversion
#> Thm.prop_of
#> snd o Logic.dest_equals
- #> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
+ #> Simplifier.rewrite_term (Proof_Context.theory_of
(empty_simpset ctxt addsimps rewrite_rules (*@ @{thms eq_True} still useful?*))) rewrite_rules []
@@ -47,7 +47,7 @@
#> Thm.eta_long_conversion
#> Thm.prop_of
#> snd o Logic.dest_equals
- #> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
+ #> Simplifier.rewrite_term (Proof_Context.theory_of
(empty_simpset ctxt addsimps rewrite_rules @ @{thms eq_True})) rewrite_rules []
in (expand th) aconv (normalize th') end
--- a/src/HOL/Tools/SMT/lethe_replay_methods.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/lethe_replay_methods.ML Wed May 21 10:30:34 2025 +0200
@@ -991,7 +991,7 @@
|> empty_simpset
|> put_simpset HOL_basic_ss
|> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel})
- |> Raw_Simplifier.add_eqcong @{thm verit_ite_if_cong}
+ |> Simplifier.add_eqcong @{thm verit_ite_if_cong}
|> Simplifier.full_simp_tac
in
SMT_Replay_Methods.prove ctxt t (fn _ => simplify_ite ctxt []
@@ -1128,7 +1128,7 @@
ctxt
|> empty_simpset
|> put_simpset HOL_basic_ss
- |> Raw_Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]}
+ |> Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]}
|> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms})
|> Simplifier.full_simp_tac
--- a/src/HOL/Tools/SMT/smt_normalize.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed May 21 10:30:34 2025 +0200
@@ -257,7 +257,7 @@
Thm.forall_intr_vars #>
Conv.fconv_rule (gen_normalize1_conv ctxt) #>
(* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
- Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
+ Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
fun gen_norm1_safe ctxt (i, thm) =
(case try (gen_normalize1 ctxt) thm of
--- a/src/HOL/Tools/SMT/smtlib_isar.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/smtlib_isar.ML Wed May 21 10:30:34 2025 +0200
@@ -43,7 +43,7 @@
fun postprocess_step_conclusion ctxt rewrite_rules ll_defs =
let val thy = Proof_Context.theory_of ctxt in
- Raw_Simplifier.rewrite_term thy rewrite_rules []
+ Simplifier.rewrite_term thy rewrite_rules []
#> Object_Logic.atomize_term ctxt
#> not (null ll_defs) ? unlift_term ll_defs
#> simplify_bool
--- a/src/HOL/Tools/SMT/verit_replay.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/verit_replay.ML Wed May 21 10:30:34 2025 +0200
@@ -45,14 +45,14 @@
let
val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> id)
val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy rewrite_rules []
+ Simplifier.rewrite_term thy rewrite_rules []
#> not (null ll_defs andalso Lethe_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
end
val rewrite_concl = if Lethe_Proof.keep_app_symbols rule then
filter (curry Term.could_unify (Thm.concl_of @{thm SMT.fun_app_def}) o Thm.concl_of) rewrite_rules
else rewrite_rules
val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy rewrite_concl []
+ Simplifier.rewrite_term thy rewrite_concl []
#> Object_Logic.atomize_term ctxt
#> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
#> SMTLIB_Isar.unskolemize_names ctxt
@@ -104,7 +104,7 @@
(ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes))))
val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy ((if Lethe_Proof.keep_raw_lifting rule then tl rewrite_rules else rewrite_rules)) []
+ Simplifier.rewrite_term thy ((if Lethe_Proof.keep_raw_lifting rule then tl rewrite_rules else rewrite_rules)) []
#> Object_Logic.atomize_term ctxt
#> not (null ll_defs andalso Lethe_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
#> SMTLIB_Isar.unskolemize_names ctxt
@@ -161,7 +161,7 @@
val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state
val global_transformer = subst_only_free global_transformation
val rewrite = let val thy = Proof_Context.theory_of ctxt in
- Raw_Simplifier.rewrite_term thy (rewrite_rules) []
+ Simplifier.rewrite_term thy (rewrite_rules) []
#> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
end
val start0 = Timing.start ()
@@ -197,7 +197,7 @@
fun replay_assumed assms ll_defs rewrite_rules stats ctxt term =
let
val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy rewrite_rules []
+ Simplifier.rewrite_term thy rewrite_rules []
#> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
end
val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term))
@@ -243,7 +243,7 @@
prems = [],
proof_ctxt = [],
concl = Thm.prop_of th
- |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
+ |> Simplifier.rewrite_term (Proof_Context.theory_of
(empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [],
bounds = [],
insts = Symtab.empty,
@@ -251,7 +251,7 @@
subproof = ([], [], [], [])}
val used_assert_ids = fold add_used_asserts_in_step actual_steps []
fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
- Raw_Simplifier.rewrite_term thy rewrite_rules [] end
+ Simplifier.rewrite_term thy rewrite_rules [] end
val used_assm_js =
map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME (i, nth assms i)
else NONE end)
--- a/src/HOL/Tools/Transfer/transfer.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed May 21 10:30:34 2025 +0200
@@ -246,7 +246,7 @@
val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
val cprop = Thm.cterm_of ctxt prop2
- val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false @{thms is_equality_lemma} cprop
+ val equal_thm = Simplifier.rewrite_wrt ctxt false @{thms is_equality_lemma} cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
in
forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -333,7 +333,7 @@
val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
val prop2 = Logic.list_rename_params (rev names) prop1
val cprop = Thm.cterm_of ctxt prop2
- val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false @{thms Domainp_lemma} cprop
+ val equal_thm = Simplifier.rewrite_wrt ctxt false @{thms Domainp_lemma} cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
in
forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -693,7 +693,7 @@
|> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
val thm2 = thm1
|> Thm.instantiate (TVars.make instT, Vars.empty)
- |> Raw_Simplifier.rewrite_rule ctxt pre_simps
+ |> Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val rule = transfer_rule_of_lhs ctxt' (HOLogic.dest_Trueprop (Thm.concl_of thm2))
in
@@ -707,7 +707,7 @@
THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) =>
raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
- |> Raw_Simplifier.rewrite_rule ctxt' post_simps
+ |> Simplifier.rewrite_rule ctxt' post_simps
|> Simplifier.norm_hhf ctxt'
|> Drule.generalize
(Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
@@ -728,7 +728,7 @@
|> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
val thm2 = thm1
|> Thm.instantiate (TVars.make instT, Vars.empty)
- |> Raw_Simplifier.rewrite_rule ctxt pre_simps
+ |> Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
val rule = transfer_rule_of_term ctxt' true t
@@ -743,7 +743,7 @@
THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) =>
raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
- |> Raw_Simplifier.rewrite_rule ctxt' post_simps
+ |> Simplifier.rewrite_rule ctxt' post_simps
|> Simplifier.norm_hhf ctxt'
|> Drule.generalize
(Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
--- a/src/HOL/Tools/inductive.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/inductive.ML Wed May 21 10:30:34 2025 +0200
@@ -333,7 +333,7 @@
val bad_app = "Inductive predicate must be applied to parameter(s) ";
-fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize [];
+fun atomize_term thy = Simplifier.rewrite_term thy inductive_atomize [];
in
--- a/src/HOL/Tools/nat_arith.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/nat_arith.ML Wed May 21 10:30:34 2025 +0200
@@ -19,7 +19,7 @@
fun move_to_front ctxt path = Conv.every_conv
[Conv.rewr_conv (Library.foldl (op RS) (@{thm nat_arith.rule0}, path)),
- Conv.arg_conv (Raw_Simplifier.rewrite_wrt ctxt false norm_rules)]
+ Conv.arg_conv (Simplifier.rewrite_wrt ctxt false norm_rules)]
fun add_atoms path \<^Const_>\<open>plus _ for x y\<close> =
add_atoms (@{thm nat_arith.add1}::path) x #>
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Wed May 21 10:30:34 2025 +0200
@@ -438,7 +438,7 @@
val (t', ctxt') = yield_singleton (Variable.import_terms true) t (Variable.declare_term t ctxt)
val ct = Thm.cterm_of ctxt' t'
fun unfold_conv thms =
- Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
+ Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
(empty_simpset ctxt' addsimps thms)
val prep_eq = (comprehension_conv ctxt' then_conv unfold_conv prep_thms) ct
val t'' = Thm.term_of (Thm.rhs_of prep_eq)
@@ -476,7 +476,7 @@
fun code_proc ctxt redex =
let
fun unfold_conv thms =
- Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
+ Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
(empty_simpset ctxt addsimps thms)
val prep_thm = unfold_conv @{thms eq_equal[symmetric]} redex
in
--- a/src/HOL/Tools/simpdata.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/simpdata.ML Wed May 21 10:30:34 2025 +0200
@@ -35,7 +35,7 @@
val ex_comm = @{thm ex_comm}
val atomize =
let val rules = @{thms atomize_all atomize_imp atomize_eq atomize_conj}
- in fn ctxt => Raw_Simplifier.rewrite_wrt ctxt true rules end
+ in fn ctxt => Simplifier.rewrite_wrt ctxt true rules end
);
structure Simpdata =
--- a/src/HOL/Types_To_Sets/Examples/Prerequisites.thy Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy Wed May 21 10:30:34 2025 +0200
@@ -79,7 +79,7 @@
end
fun var_simplify_only ctxt ths thm =
- asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm
+ asm_full_var_simplify (Simplifier.clear_simpset ctxt addsimps ths) thm
val var_simplified = Attrib.thms >>
(fn ths => Thm.rule_attribute ths
--- a/src/HOL/Types_To_Sets/unoverload_type.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML Wed May 21 10:30:34 2025 +0200
@@ -47,7 +47,7 @@
|> map varify_const
in
fold Unoverloading.unoverload consts thm''
- |> Raw_Simplifier.norm_hhf (Context.proof_of context)
+ |> Simplifier.norm_hhf (Context.proof_of context)
end
end
--- a/src/Pure/ex/Guess.thy Wed May 21 10:30:33 2025 +0200
+++ b/src/Pure/ex/Guess.thy Wed May 21 10:30:34 2025 +0200
@@ -152,7 +152,7 @@
ctxt' (k, [(s, [th])]);
val before_qed =
Method.primitive_text (fn ctxt =>
- Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
+ Goal.conclude #> Simplifier.norm_hhf ctxt #>
(fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)));
fun after_qed (result_ctxt, results) state' =
let
--- a/src/Pure/simplifier.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/Pure/simplifier.ML Wed May 21 10:30:34 2025 +0200
@@ -157,10 +157,10 @@
(* simproc_setup with concrete syntax *)
val simproc_setup =
- Named_Target.setup_result Raw_Simplifier.transform_simproc o define_simproc;
+ Named_Target.setup_result transform_simproc o define_simproc;
fun simproc_setup_cmd args =
- Named_Target.setup_result Raw_Simplifier.transform_simproc
+ Named_Target.setup_result transform_simproc
(fn lthy => lthy |> define_simproc (read_simproc_spec lthy args));
val parse_proc_kind =
@@ -310,20 +310,20 @@
fun solve_all_tac solvers ctxt =
let
- val subgoal_tac = Raw_Simplifier.subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt);
+ val subgoal_tac = subgoal_tac (set_solvers solvers ctxt);
val solve_tac = subgoal_tac THEN_ALL_NEW (K no_tac);
in DEPTH_SOLVE (solve_tac 1) end;
(*NOTE: may instantiate unknowns that appear also in other subgoals*)
fun generic_simp_tac safe mode ctxt =
let
- val loop_tac = Raw_Simplifier.loop_tac ctxt;
- val (unsafe_solvers, solvers) = Raw_Simplifier.solvers ctxt;
- val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt)
+ val loop_tac = loop_tac ctxt;
+ val (unsafe_solvers, solvers) = solvers ctxt;
+ val solve_tac = FIRST' (map (solver ctxt)
(rev (if safe then solvers else unsafe_solvers)));
fun simp_loop_tac i =
- Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN
+ generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN
(solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
in PREFER_GOAL (simp_loop_tac 1) end;
@@ -331,15 +331,15 @@
fun simp rew mode ctxt thm =
let
- val (unsafe_solvers, _) = Raw_Simplifier.solvers ctxt;
+ val (unsafe_solvers, _) = solvers ctxt;
val tacf = solve_all_tac (rev unsafe_solvers);
fun prover s th = Option.map #1 (Seq.pull (tacf s th));
in rew mode prover ctxt thm end;
in
-val simp_thm = simp Raw_Simplifier.rewrite_thm;
-val simp_cterm = simp Raw_Simplifier.rewrite_cterm;
+val simp_thm = simp rewrite_thm;
+val simp_cterm = simp rewrite_cterm;
end;
@@ -398,7 +398,7 @@
(Args.del -- Args.colon >> K del_proc ||
Scan.option (Args.add -- Args.colon) >> K add_proc)
>> (fn f => fn simproc => Morphism.entity (fn phi => Thm.declaration_attribute
- (K (Raw_Simplifier.map_ss (f (transform_simproc phi simproc))))));
+ (K (map_ss (f (transform_simproc phi simproc))))));
in
@@ -425,7 +425,7 @@
val simplified = conv_mode -- Attrib.thms >>
(fn (f, ths) => Thm.rule_attribute ths (fn context =>
- f ((if null ths then I else Raw_Simplifier.clear_simpset)
+ f ((if null ths then I else clear_simpset)
(Context.proof_of context) addsimps ths)));
end;
@@ -460,7 +460,7 @@
Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
Args.$$$ simpN -- Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
- K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
+ K {init = clear_simpset, attribute = simp_add, pos = \<^here>}]
@ cong_modifiers;
val simp_modifiers' =
@@ -468,7 +468,7 @@
Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
Args.$$$ onlyN -- Args.colon >>
- K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
+ K {init = clear_simpset, attribute = simp_add, pos = \<^here>}]
@ cong_modifiers;
val simp_options =
@@ -500,12 +500,12 @@
"simplification (all goals)";
fun unsafe_solver_tac ctxt =
- FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
+ FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: prems_of ctxt), assume_tac ctxt];
val unsafe_solver = mk_solver "Pure unsafe" unsafe_solver_tac;
(*no premature instantiation of variables during simplification*)
fun safe_solver_tac ctxt =
- FIRST' [match_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), eq_assume_tac];
+ FIRST' [match_tac ctxt (Drule.reflexive_thm :: prems_of ctxt), eq_assume_tac];
val safe_solver = mk_solver "Pure safe" safe_solver_tac;
val _ =
--- a/src/Tools/Code/code_runtime.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/Tools/Code/code_runtime.ML Wed May 21 10:30:34 2025 +0200
@@ -362,7 +362,7 @@
fun preprocess_conv { ctxt } =
let
val rules = get ctxt;
- in fn ctxt' => Raw_Simplifier.rewrite_wrt ctxt' false rules end;
+ in fn ctxt' => Simplifier.rewrite_wrt ctxt' false rules end;
fun preprocess_term { ctxt } =
let
--- a/src/Tools/atomize_elim.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/Tools/atomize_elim.ML Wed May 21 10:30:34 2025 +0200
@@ -54,7 +54,7 @@
*)
fun atomize_elim_conv ctxt ct =
(forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
- then_conv Raw_Simplifier.rewrite_wrt ctxt true (Named_Theorems.get ctxt named_theorems)
+ then_conv Simplifier.rewrite_wrt ctxt true (Named_Theorems.get ctxt named_theorems)
then_conv (fn ct' => if can (Object_Logic.dest_judgment ctxt) ct'
then all_conv ct'
else raise CTERM ("atomize_elim", [ct', ct])))
--- a/src/Tools/coherent.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/Tools/coherent.ML Wed May 21 10:30:34 2025 +0200
@@ -42,7 +42,7 @@
if is_atomic (Logic.strip_imp_concl (Thm.term_of ct)) then Conv.all_conv ct
else Conv.concl_conv (length (Logic.strip_imp_prems (Thm.term_of ct)))
(Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
- Raw_Simplifier.rewrite_wrt ctxt true (map Thm.symmetric
+ Simplifier.rewrite_wrt ctxt true (map Thm.symmetric
[Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
fun rulify_elim ctxt th = Simplifier.norm_hhf ctxt (Conv.fconv_rule (rulify_elim_conv ctxt) th);
--- a/src/Tools/induct.ML Wed May 21 10:30:33 2025 +0200
+++ b/src/Tools/induct.ML Wed May 21 10:30:34 2025 +0200
@@ -442,10 +442,10 @@
fun mark_constraints n ctxt = Conv.fconv_rule
(Conv.prems_conv ~1 (Conv.params_conv ~1 (fn ctxt' =>
- Conv.prems_conv n (Raw_Simplifier.rewrite_wrt ctxt' false [equal_def'])) ctxt));
+ Conv.prems_conv n (Simplifier.rewrite_wrt ctxt' false [equal_def'])) ctxt));
fun unmark_constraints ctxt =
- Conv.fconv_rule (Raw_Simplifier.rewrite_wrt ctxt true [Induct_Args.equal_def]);
+ Conv.fconv_rule (Simplifier.rewrite_wrt ctxt true [Induct_Args.equal_def]);
(* simplify *)
@@ -546,10 +546,10 @@
(* atomize *)
fun atomize_term ctxt =
- Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize []
+ Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize []
#> Object_Logic.drop_judgment ctxt;
-fun atomize_cterm ctxt = Raw_Simplifier.rewrite_wrt ctxt true Induct_Args.atomize;
+fun atomize_cterm ctxt = Simplifier.rewrite_wrt ctxt true Induct_Args.atomize;
fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize;
@@ -560,8 +560,8 @@
(* rulify *)
fun rulify_term thy =
- Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
- Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
+ Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
+ Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
fun rulified_term ctxt thm =
let
@@ -702,7 +702,7 @@
fun miniscope_tac p =
CONVERSION o
Conv.params_conv p (fn ctxt =>
- Raw_Simplifier.rewrite_wrt ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
+ Simplifier.rewrite_wrt ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
in