src/FOL/simpdata.ML
changeset 4649 89ad3eb863a1
parent 4477 b3e5857d8d99
child 4652 d24cca140eeb
     1.1 --- a/src/FOL/simpdata.ML	Tue Feb 24 11:35:33 1998 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Wed Feb 25 15:45:32 1998 +0100
     1.3 @@ -334,8 +334,9 @@
     1.4  
     1.5  (*Add a simpset to a classical set!*)
     1.6  infix 4 addSss addss;
     1.7 -fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
     1.8 -fun cs addss  ss = cs addbefore                        asm_full_simp_tac ss;
     1.9 +fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
    1.10 +				  CHANGED o (safe_asm_more_full_simp_tac ss));
    1.11 +fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", asm_full_simp_tac ss);
    1.12  
    1.13  fun Addss ss = (claset_ref() := claset() addss ss);
    1.14