# HG changeset patch
# User wenzelm
# Date 1752571322 -7200
# Node ID 898d3860a2042945b49e2265643b5a174b617397
# Parent  df8de6dacede1a3496517670fba858a51a0ff289
tuned (see also 9e7d1c139569);

diff -r df8de6dacede -r 898d3860a204 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Tue Jul 15 11:11:56 2025 +0200
+++ b/src/Provers/clasimp.ML	Tue Jul 15 11:22:02 2025 +0200
@@ -43,13 +43,15 @@
 
 (* simp as classical wrapper *)
 
-(* FIXME !? *)
-fun clasimp f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt));
-
-(*Add a simpset to the claset!*)
 (*Caution: only one simpset added can be added by each of addSss and addss*)
-val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
-val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
+local
+  fun add_wrapper f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt));
+in
+  val addSss =
+    add_wrapper Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
+  val addss =
+    add_wrapper Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
+end;
 
 
 (* iffs: addition of rules to simpsets and clasets simultaneously *)