# HG changeset patch
# User wenzelm
# Date 1749725634 -7200
# Node ID 032c2aac4454a03adf0d0bd3a6cac9b15cd79627
# Parent  d93ead9ac6df72a1b379b4f0328cfc942f22bba7
avoid legacy infixes;

diff -r d93ead9ac6df -r 032c2aac4454 src/Sequents/Sequents.thy
--- 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]]
diff -r d93ead9ac6df -r 032c2aac4454 src/Sequents/simpdata.ML
--- 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;