# HG changeset patch
# User paulson
# Date 906725160 -7200
# Node ID 99c6ef61288fe14ca8104583634152627a9eb7c4
# Parent  d176d9d17181f0407cb7b9c1abc193041c7f52a8
deleted illegal "op"

diff -r d176d9d17181 -r 99c6ef61288f src/Provers/clasimp.ML
--- 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 *)