# HG changeset patch
# User wenzelm
# Date 1749725957 -7200
# Node ID cc05bc2cfb2f23106ecef0c06b822b7809287d84
# Parent  032c2aac4454a03adf0d0bd3a6cac9b15cd79627
clarified modules;

diff -r 032c2aac4454 -r cc05bc2cfb2f src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Jun 12 12:53:54 2025 +0200
+++ b/src/FOL/IFOL.thy	Thu Jun 12 12:59:17 2025 +0200
@@ -9,7 +9,6 @@
   abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1"
 begin
 
-ML_file \<open>~~/src/Tools/simp_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Provers/splitter.ML\<close>
 ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
diff -r 032c2aac4454 -r cc05bc2cfb2f src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Thu Jun 12 12:53:54 2025 +0200
+++ b/src/FOLP/IFOLP.thy	Thu Jun 12 12:59:17 2025 +0200
@@ -9,7 +9,6 @@
 imports Pure
 begin
 
-ML_file \<open>~~/src/Tools/simp_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 
 setup Pure_Thy.old_appl_syntax_setup
diff -r 032c2aac4454 -r cc05bc2cfb2f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jun 12 12:53:54 2025 +0200
+++ b/src/HOL/HOL.thy	Thu Jun 12 12:59:17 2025 +0200
@@ -13,7 +13,6 @@
 abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1"
 begin
 
-ML_file \<open>~~/src/Tools/simp_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/try.ML\<close>
 ML_file \<open>~~/src/Tools/quickcheck.ML\<close>
diff -r 032c2aac4454 -r cc05bc2cfb2f src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Thu Jun 12 12:53:54 2025 +0200
+++ b/src/Tools/misc_legacy.ML	Thu Jun 12 12:59:17 2025 +0200
@@ -3,6 +3,15 @@
 Misc legacy stuff -- to be phased out eventually.
 *)
 
+infix 4 addsimps delsimps addsimprocs delsimprocs;
+
+fun ctxt addsimps thms = ctxt |> Simplifier.add_simps thms;
+fun ctxt delsimps thms = ctxt |> Simplifier.del_simps thms;
+
+fun ctxt addsimprocs procs = ctxt |> fold Simplifier.add_proc procs;
+fun ctxt delsimprocs procs = ctxt |> fold Simplifier.del_proc procs;
+
+
 signature MISC_LEGACY =
 sig
   val add_term_names: term * string list -> string list
diff -r 032c2aac4454 -r cc05bc2cfb2f src/Tools/simp_legacy.ML
--- a/src/Tools/simp_legacy.ML	Thu Jun 12 12:53:54 2025 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(*  Title:      Tools/simp_legacy.ML
-
-Legacy simplifier configuration interfaces -- to be phased out eventually.
-*)
-
-infix 4 addsimps delsimps addsimprocs delsimprocs;
-
-fun ctxt addsimps thms = ctxt |> Simplifier.add_simps thms;
-fun ctxt delsimps thms = ctxt |> Simplifier.del_simps thms;
-
-fun ctxt addsimprocs procs = ctxt |> fold Simplifier.add_proc procs;
-fun ctxt delsimprocs procs = ctxt |> fold Simplifier.del_proc procs;