--- 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>
--- 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
--- 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>
--- 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
--- 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;