--- a/src/FOL/simpdata.ML Tue Feb 24 11:35:33 1998 +0100
+++ b/src/FOL/simpdata.ML Wed Feb 25 15:45:32 1998 +0100
@@ -334,8 +334,9 @@
(*Add a simpset to a classical set!*)
infix 4 addSss addss;
-fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
-fun cs addss ss = cs addbefore asm_full_simp_tac ss;
+fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
+ CHANGED o (safe_asm_more_full_simp_tac ss));
+fun cs addss ss = cs addbefore ("asm_full_simp_tac", asm_full_simp_tac ss);
fun Addss ss = (claset_ref() := claset() addss ss);