1.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Wed Dec 05 10:21:35 2012 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Wed Dec 05 15:29:36 2012 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  	fun coeff_in c v = member op = (vars c) v;
     1.5     	fun finddivide (_ $ _ $ _ $ _) v = error("is_rateqation_in:")
     1.6  	    (* at the moment there is no term like this, but ....*)
     1.7 -	  | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v
     1.8 +	  | finddivide (t as (Const ("Fields.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v
     1.9  	  | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) 
    1.10                                           orelse (finddivide t2 v)
    1.11  	  | finddivide (_ $ t1) v = (finddivide t1 v)
    1.12 @@ -106,7 +106,7 @@
    1.13  	(merge_rls "is_ratequation_in" calculate_Rational
    1.14  		   (append_rls "is_ratequation_in"
    1.15  			Poly_erls
    1.16 -			[(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*)
    1.17 +			[(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)
    1.18  			 Calc ("RatEq.is'_ratequation'_in",
    1.19  			       eval_is_ratequation_in "")
    1.20  
    1.21 @@ -124,7 +124,7 @@
    1.22  	(merge_rls "is_ratequation_in" calculate_Rational
    1.23  		   (append_rls "is_ratequation_in"
    1.24  			Poly_erls
    1.25 -			[(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*)
    1.26 +			[(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)
    1.27  			 Calc ("RatEq.is'_ratequation'_in",
    1.28  			       eval_is_ratequation_in "")
    1.29  			 ]))