diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -55,7 +55,7 @@
    [Thm  ("real_assoc_1",num_str @{thm real_assoc_1})
     (*		
      Don't use
-     Calc ("HOL.divide", eval_cancel "#divide_e"),
+     Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
      Calc ("Atools.pow" ,eval_binop "#power_"),
      *)
     ];
@@ -66,7 +66,7 @@
    [Thm  ("real_assoc_1",num_str @{thm real_assoc_1})
     (*		
      Don't use
-     Calc ("HOL.divide", eval_cancel "#divide_e"),
+     Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
      Calc ("Atools.pow" ,eval_binop "#power_"),
      *)
     ];
@@ -84,11 +84,11 @@
        (*asm_thm = [],*)
        rules = [
 		Thm  ("real_assoc_1",num_str @{thm real_assoc_1}),
-		Calc ("op +",eval_binop "#add_"),
-		Calc ("op -",eval_binop "#sub_"),
+		Calc ("Groups.plus_class.plus",eval_binop "#add_"),
+		Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
 		Calc ("op *",eval_binop "#mult_"),
 		(*  Dont use  
-		 Calc ("HOL.divide", eval_cancel "#divide_e"),		
+		 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),		
 		 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
 		 *)
 		Calc ("Atools.pow" ,eval_binop "#power_")