1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4  fun is_rootTerm_in t v = 
     1.5      let 
     1.6  	fun coeff_in c v = member op = (vars c) v;
     1.7 -   	fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:")
     1.8 +   	fun findroot (_ $ _ $ _ $ _) v = error("is_rootTerm_in:")
     1.9  	  (* at the moment there is no term like this, but ....*)
    1.10  	  | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v
    1.11  	  | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v)
    1.12 @@ -139,7 +139,7 @@
    1.13   fun is_sqrtTerm_in t v = 
    1.14      let 
    1.15  	fun coeff_in c v = member op = (vars c) v;
    1.16 -   	fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:")
    1.17 +   	fun findsqrt (_ $ _ $ _ $ _) v = error("is_sqrteqation_in:")
    1.18  	  (* at the moment there is no term like this, but ....*)
    1.19  	  | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
    1.20  	  | findsqrt (t as (Const ("NthRoot.sqrt",_) $ a)) v = coeff_in a v
    1.21 @@ -154,7 +154,7 @@
    1.22   fun is_normSqrtTerm_in t v =
    1.23       let
    1.24  	fun coeff_in c v = member op = (vars c) v;
    1.25 -        fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
    1.26 +        fun isnorm (_ $ _ $ _ $ _) v = error("is_normSqrtTerm_in:")
    1.27  	  (* at the moment there is no term like this, but ....*)
    1.28            | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
    1.29            | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v