diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/RootEq.thy
--- a/src/Tools/isac/Knowledge/RootEq.thy	Tue Sep 28 10:01:18 2010 +0200
+++ b/src/Tools/isac/Knowledge/RootEq.thy	Tue Sep 28 10:10:26 2010 +0200
@@ -157,7 +157,7 @@
         fun isnorm (_ $ _ $ _ $ _) v = error("is_normSqrtTerm_in:")
 	  (* at the moment there is no term like this, but ....*)
           | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
-          | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
+          | isnorm (Const ("Groups.times_class.times",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
           | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false
           | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse 
                               (is_sqrtTerm_in t2 v)
@@ -447,7 +447,7 @@
                              (* a*(b*c) = a*b*c *)
                 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
                 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
-                Calc ("op *",eval_binop "#mult_"),
+                Calc ("Groups.times_class.times",eval_binop "#mult_"),
                 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
                 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
                 Calc ("Atools.pow" ,eval_binop "#power_"),