--- a/src/Sequents/Sequents.thy Thu Jun 12 12:44:47 2025 +0200
+++ b/src/Sequents/Sequents.thy Thu Jun 12 12:53:54 2025 +0200
@@ -10,8 +10,6 @@
keywords "print_pack" :: diag
begin
-ML_file \<open>~~/src/Tools/simp_legacy.ML\<close>
-
setup Pure_Thy.old_appl_syntax_setup
declare [[unify_trace_bound = 20, unify_search_bound = 40]]
--- a/src/Sequents/simpdata.ML Thu Jun 12 12:44:47 2025 +0200
+++ b/src/Sequents/simpdata.ML Thu Jun 12 12:53:54 2025 +0200
@@ -85,7 +85,8 @@
@{thms LK_extra_simps};
val LK_ss =
- put_simpset LK_basic_ss \<^context> addsimps LK_simps
+ put_simpset LK_basic_ss \<^context>
+ |> Simplifier.add_simps LK_simps
|> Simplifier.add_eqcong @{thm left_cong}
|> Simplifier.add_cong @{thm imp_cong}
|> simpset_of;