diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -140,7 +140,7 @@
 		  Thm ("integral_add",num_str @{thm integral_add}),
 		  Thm ("integral_mult",num_str @{thm integral_mult}),
 		  Thm ("integral_pow",num_str @{thm integral_pow}),
-		  Calc ("op +", eval_binop "#add_")(*for n+1*)
+		  Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
 		  ],
 	 scr = EmptyScr};
 *}
@@ -200,7 +200,7 @@
 	       Thm ("divide_divide_eq_left",
                      num_str @{thm divide_divide_eq_left}),
 	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e"),
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),
 	      
 	       Thm ("rat_power", num_str @{thm rat_power})
 		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
@@ -264,7 +264,7 @@
 	       Rls_ discard_parentheses,
 	       (*Rls_ collect_bdv, from make_polynomial_in*)
 	       Rls_ separate_bdv2,
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
 	       ],
       scr = EmptyScr}:rls;      
 
@@ -302,7 +302,7 @@
 * 				 num_str @{thm add_divide_distrib})
 * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
 * 			  ]),
-* 	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
+* 	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
 * 	       ],
 *       scr = EmptyScr
 *       }:rls);