diff -r 95d956108461 -r 460c24a6a6ba src/Tools/isac/Interpret/mathengine.sml
--- a/src/Tools/isac/Interpret/mathengine.sml	Tue Sep 28 08:58:06 2010 +0200
+++ b/src/Tools/isac/Interpret/mathengine.sml	Tue Sep 28 09:06:56 2010 +0200
@@ -140,7 +140,7 @@
 (*----------------------------------------------------from solve.sml*)
   | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) =
     let (*val rls = the (assoc(!ruleset',rls'))
-	    handle _ => raise error ("solve: '"^rls'^"' not known");*)
+	    handle _ => error ("solve: '"^rls'^"' not known");*)
 	val thy = assoc_thy thy';
         val (srls, sc, is) = 
 	    case rls of
@@ -154,7 +154,7 @@
 	val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);
 	val aopt = applicable_in p pt nx;
     in case aopt of
-	   Notappl s => raise error ("solve Detail_Set: "^s)
+	   Notappl s => error ("solve Detail_Set: "^s)
 	 (* val Appl m = aopt;
 	    *)
 	 | Appl m => solve ("discardFIXME",m) p pt end
@@ -473,16 +473,16 @@
 	      | ("unsafe-ok", (_, _, ptp)) => ptp
 	      | ("not-applicable",_) => (pt, p)
 	      | ("end-of-calculation", (_, _, ptp)) => ptp
-	      | ("failure",_) => raise error "sys-error";
+	      | ("failure",_) => error "sys-error";
 	val (_, ts) = 
 (* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]);
    *)
 	    (case step p ((pt, e_pos'),[]) of
 		 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
 	       | ("helpless",_) => ("helpless: cannot propose tac", [])
-	       | ("no-fmz-spec",_) => raise error "no-fmz-spec"
+	       | ("no-fmz-spec",_) => error "no-fmz-spec"
 	       | ("end-of-calculation", (ts, _, _)) => ("",ts))
-	    handle _ => raise error "sys-error";
+	    handle _ => error "sys-error";
 	val tac = case ts of tacis as (_::_) =>
 (* val tacis as (_::_) = ts;
    *)