1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  	  | rootadd (t as (Const ("Groups.minus_class.minus",_) $ t2 $ t3)) v = 
     1.5              (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
     1.6  	  | rootadd _ _ = false;
     1.7 -	fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:")
     1.8 +	fun findrootrat (_ $ _ $ _ $ _) v = error("is_rootRatAddTerm_in:")
     1.9  	  (* at the moment there is no term like this, but ....*)
    1.10  	  | findrootrat (t as (Const ("Rings.inverse_class.divide",_) $ _ $ t3)) v = 
    1.11  	               if (is_rootTerm_in t3 v) then rootadd t3 v else false