# HG changeset patch # User haftmann # Date 1747816234 -7200 # Node ID f1c14af175919ca36b9d6f1a8c6501c005c6b2b6 # Parent e478f85fe4274c4c9ae5681ca0d4b39ea1338668 prefer Simplifier over bootstrap-only Raw_Simplifier diff -r e478f85fe427 -r f1c14af17591 src/FOL/simpdata.ML --- 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 ); diff -r e478f85fe427 -r f1c14af17591 src/HOL/Library/conditional_parametricity.ML --- 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})) diff -r e478f85fe427 -r f1c14af17591 src/HOL/Library/old_recdef.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Nominal/nominal_inductive.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Nominal/nominal_inductive2.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Nonstandard_Analysis/transfer_principle.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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 "\x. P x \ 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; diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- 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) diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML --- 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>\Main\)) - |> 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' @ diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- 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); diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Function/induction_schema.ML --- 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 = diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Function/partial_function.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Lifting/lifting_def.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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>\If\, _)) => 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/cvc5_replay.ML --- 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) diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/cvc_proof_parse.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/lethe_replay_methods.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/smt_normalize.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/smtlib_isar.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/verit_replay.ML --- 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) diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Transfer/transfer.ML --- 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) diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/inductive.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/nat_arith.ML --- 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_>\plus _ for x y\ = add_atoms (@{thm nat_arith.add1}::path) x #> diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/set_comprehension_pointfree.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/simpdata.ML --- 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 = diff -r e478f85fe427 -r f1c14af17591 src/HOL/Types_To_Sets/Examples/Prerequisites.thy --- 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 diff -r e478f85fe427 -r f1c14af17591 src/HOL/Types_To_Sets/unoverload_type.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/Pure/ex/Guess.thy --- 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 diff -r e478f85fe427 -r f1c14af17591 src/Pure/simplifier.ML --- 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 _ = diff -r e478f85fe427 -r f1c14af17591 src/Tools/Code/code_runtime.ML --- 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 diff -r e478f85fe427 -r f1c14af17591 src/Tools/atomize_elim.ML --- 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]))) diff -r e478f85fe427 -r f1c14af17591 src/Tools/coherent.ML --- 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); diff -r e478f85fe427 -r f1c14af17591 src/Tools/induct.ML --- 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