1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4  (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
     1.5  fun is_polyrat_in t v = 
     1.6      let fun coeff_in c v = member op = (vars c) v;
     1.7 -   	fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")
     1.8 +   	fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:")
     1.9  	    (* at the moment there is no term like this, but ....*)
    1.10  	  | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = 
    1.11              not(coeff_in b v)
    1.12 @@ -1141,7 +1141,7 @@
    1.13    | get_basStr (Free (str, _)) = str
    1.14    | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *)
    1.15  (*| get_basStr t = 
    1.16 -    raise error("get_basStr: called with t= "^(term2str t));*)
    1.17 +    error("get_basStr: called with t= "^(term2str t));*)
    1.18  
    1.19  (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
    1.20  fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
    1.21 @@ -1149,7 +1149,7 @@
    1.22    | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
    1.23    | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *)
    1.24  (*| get_potStr t = 
    1.25 -    raise error("get_potStr: called with t= "^(term2str t));*)
    1.26 +    error("get_potStr: called with t= "^(term2str t));*)
    1.27  
    1.28  (* Umgekehrte string_ord *)
    1.29  val string_ord_rev =  rev_order o string_ord;
    1.30 @@ -1208,7 +1208,7 @@
    1.31  	       | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) => 
    1.32  		     counter (n + 1000, xs) (*FIXME.MG?!*)
    1.33  	       | (Free (str, _)) => counter (n + 1, xs)
    1.34 -	     (*| _ => raise error("monom_degree: called with factor: "^(term2str x)))*)
    1.35 +	     (*| _ => error("monom_degree: called with factor: "^(term2str x)))*)
    1.36  	       | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
    1.37  in  
    1.38      fun monom_degree l = counter (0, l) 
    1.39 @@ -1240,7 +1240,7 @@
    1.40  fun tl_str str = substring (str, 1, (size str) - 1);
    1.41  
    1.42  (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
    1.43 -fun get_koeff_of_mon [] =  raise error("get_koeff_of_mon: called with l = []")
    1.44 +fun get_koeff_of_mon [] =  error("get_koeff_of_mon: called with l = []")
    1.45    | get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x
    1.46  				    else NONE;
    1.47