--- a/src/Provers/clasimp.ML Fri Sep 25 14:05:34 1998 +0200
+++ b/src/Provers/clasimp.ML Fri Sep 25 14:06:00 1998 +0200
@@ -75,9 +75,9 @@
(*Add a simpset to a classical set!*)
(*Caution: only one simpset added can be added by each of addSss and addss*)
-fun cs addSss ss = op Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
+fun cs addSss ss = Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
CHANGED o Simplifier.safe_asm_full_simp_tac ss));
-fun cs addss ss = op Classical.addbefore (cs, ("asm_full_simp_tac",
+fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac",
CHANGED o Simplifier.asm_full_simp_tac ss));
(* tacticals *)