diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Tue Sep 28 10:01:18 2010 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Sep 28 10:10:26 2010 +0200
@@ -86,7 +86,7 @@
 		Thm  ("real_assoc_1",num_str @{thm real_assoc_1}),
 		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_"),
 		(*  Dont use  
 		 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),		
 		 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),