1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -43,14 +43,14 @@
     1.4  fun is_rootRatAddTerm_in t v = 
     1.5      let 
     1.6  	fun coeff_in c v = member op = (vars c) v;
     1.7 -	fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = 
     1.8 +	fun rootadd (t as (Const ("Groups.plus_class.plus",_) $ t2 $ t3)) v = 
     1.9              (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
    1.10 -	  | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = 
    1.11 +	  | rootadd (t as (Const ("Groups.minus_class.minus",_) $ t2 $ t3)) v = 
    1.12              (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
    1.13  	  | rootadd _ _ = false;
    1.14  	fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:")
    1.15  	  (* at the moment there is no term like this, but ....*)
    1.16 -	  | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v = 
    1.17 +	  | findrootrat (t as (Const ("Rings.inverse_class.divide",_) $ _ $ t3)) v = 
    1.18  	               if (is_rootTerm_in t3 v) then rootadd t3 v else false
    1.19  	  | findrootrat (_ $ t1 $ t2) v = 
    1.20              (findrootrat t1 v) orelse (findrootrat t2 v)