1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Feb 08 13:20:40 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Fri Feb 09 11:16:05 2018 +0100
     1.3 @@ -197,7 +197,7 @@
     1.4  	       Thm ("divide_divide_eq_left",
     1.5                       num_str @{thm divide_divide_eq_left}),
     1.6  	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
     1.7 -	       Calc ("Fields.inverse_class.divide"  ,eval_cancel "#divide_e"),
     1.8 +	       Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e"),
     1.9  	      
    1.10  	       Thm ("rat_power", num_str @{thm rat_power})
    1.11  		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
    1.12 @@ -261,7 +261,7 @@
    1.13  	       Rls_ discard_parentheses,
    1.14  	       (*Rls_ collect_bdv, from make_polynomial_in*)
    1.15  	       Rls_ separate_bdv2,
    1.16 -	       Calc ("Fields.inverse_class.divide"  ,eval_cancel "#divide_e")
    1.17 +	       Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e")
    1.18  	       ],
    1.19        scr = EmptyScr}:rls;      
    1.20  
    1.21 @@ -299,7 +299,7 @@
    1.22  * 				 num_str @{thm add_divide_distrib})
    1.23  * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
    1.24  * 			  ]),
    1.25 -* 	       Calc ("Fields.inverse_class.divide"  ,eval_cancel "#divide_e")
    1.26 +* 	       Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e")
    1.27  * 	       ],
    1.28  *       scr = EmptyScr
    1.29  *       }:rls);