diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Rational-WN.sml
--- a/src/Tools/isac/Knowledge/Rational-WN.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Rational-WN.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -63,7 +63,7 @@
     else raise error ("term2poly.2 "^term2str t)
   | mono t _ _ = raise error ("term2poly.3 "^term2str t);
 
-fun poly (Const ("op +",_) $ t1 $ t2) v g = 
+fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g = 
     let val l = mono t1 v g
     in (l @ (poly t2 v ((length l) + g))) end
   | poly t v g = mono t v g;
@@ -73,7 +73,7 @@
 				  handle _ => NONE)
   | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
     if t = v then SOME [0, (the o int_of_str) s1] else NONE
-  | term2poly (Const ("op +",_) $ (Free (s1,_)) $ t) v = 
+  | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v = 
     SOME ([(the o int_of_str) s1] @ (poly t v 1))
   | term2poly t v = 
     SOME (poly t v 0) handle _ => NONE;
@@ -144,7 +144,7 @@
 (cterm_of thy) t;
 
 
-fun mk_sum pT t1 t2 = Const ("op +", [pT, pT]--->pT) $ t1 $ t2;
+fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2;
 
 
 fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0