1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Wed Dec 05 10:21:35 2012 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Wed Dec 05 15:29:36 2012 +0100
     1.3 @@ -177,7 +177,7 @@
     1.4      let fun coeff_in c v = member op = (vars c) v;
     1.5     	fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_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 = 
     1.8 +	  | finddivide (t as (Const ("Fields.inverse_class.divide",_) $ _ $ b)) v = 
     1.9              not(coeff_in b v)
    1.10  	  | finddivide (_ $ t1 $ t2) v = 
    1.11              (finddivide t1 v) orelse (finddivide t2 v)
    1.12 @@ -1359,7 +1359,7 @@
    1.13                                      eval_is_multUnordered "")],
    1.14  	  calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")),
    1.15  		  ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
    1.16 -		  ("DIVIDE", ("Rings.inverse_class.divide", 
    1.17 +		  ("DIVIDE", ("Fields.inverse_class.divide", 
    1.18  		              eval_cancel "#divide_e")),
    1.19  		  ("POWER" , ("Atools.pow", eval_binop "#power_"))],
    1.20    errpatts = [],
    1.21 @@ -1417,7 +1417,7 @@
    1.22                                     eval_is_addUnordered "")],
    1.23  	  calc = [("PLUS"  ,("Groups.plus_class.plus", eval_binop "#add_")),
    1.24  		  ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
    1.25 -		  ("DIVIDE",("Rings.inverse_class.divide",
    1.26 +		  ("DIVIDE",("Fields.inverse_class.divide",
    1.27                                eval_cancel "#divide_e")),
    1.28  		  ("POWER" ,("Atools.pow"  ,eval_binop "#power_"))],
    1.29  	  errpatts = [],