diff -r 95d956108461 -r 460c24a6a6ba src/Tools/isac/Knowledge/Poly.thy
--- a/src/Tools/isac/Knowledge/Poly.thy	Tue Sep 28 08:58:06 2010 +0200
+++ b/src/Tools/isac/Knowledge/Poly.thy	Tue Sep 28 09:06:56 2010 +0200
@@ -175,7 +175,7 @@
 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
 fun is_polyrat_in t v = 
     let fun coeff_in c v = member op = (vars c) v;
-   	fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")
+   	fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:")
 	    (* at the moment there is no term like this, but ....*)
 	  | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = 
             not(coeff_in b v)
@@ -1141,7 +1141,7 @@
   | get_basStr (Free (str, _)) = str
   | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *)
 (*| get_basStr t = 
-    raise error("get_basStr: called with t= "^(term2str t));*)
+    error("get_basStr: called with t= "^(term2str t));*)
 
 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
 fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
@@ -1149,7 +1149,7 @@
   | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
   | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *)
 (*| get_potStr t = 
-    raise error("get_potStr: called with t= "^(term2str t));*)
+    error("get_potStr: called with t= "^(term2str t));*)
 
 (* Umgekehrte string_ord *)
 val string_ord_rev =  rev_order o string_ord;
@@ -1208,7 +1208,7 @@
 	       | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) => 
 		     counter (n + 1000, xs) (*FIXME.MG?!*)
 	       | (Free (str, _)) => counter (n + 1, xs)
-	     (*| _ => raise error("monom_degree: called with factor: "^(term2str x)))*)
+	     (*| _ => error("monom_degree: called with factor: "^(term2str x)))*)
 	       | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
 in  
     fun monom_degree l = counter (0, l) 
@@ -1240,7 +1240,7 @@
 fun tl_str str = substring (str, 1, (size str) - 1);
 
 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
-fun get_koeff_of_mon [] =  raise error("get_koeff_of_mon: called with l = []")
+fun get_koeff_of_mon [] =  error("get_koeff_of_mon: called with l = []")
   | get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x
 				    else NONE;