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