1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4  (*----------------------------------------------------from solve.sml*)
     1.5    | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) =
     1.6      let (*val rls = the (assoc(!ruleset',rls'))
     1.7 -	    handle _ => raise error ("solve: '"^rls'^"' not known");*)
     1.8 +	    handle _ => error ("solve: '"^rls'^"' not known");*)
     1.9  	val thy = assoc_thy thy';
    1.10          val (srls, sc, is) = 
    1.11  	    case rls of
    1.12 @@ -154,7 +154,7 @@
    1.13  	val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);
    1.14  	val aopt = applicable_in p pt nx;
    1.15      in case aopt of
    1.16 -	   Notappl s => raise error ("solve Detail_Set: "^s)
    1.17 +	   Notappl s => error ("solve Detail_Set: "^s)
    1.18  	 (* val Appl m = aopt;
    1.19  	    *)
    1.20  	 | Appl m => solve ("discardFIXME",m) p pt end
    1.21 @@ -473,16 +473,16 @@
    1.22  	      | ("unsafe-ok", (_, _, ptp)) => ptp
    1.23  	      | ("not-applicable",_) => (pt, p)
    1.24  	      | ("end-of-calculation", (_, _, ptp)) => ptp
    1.25 -	      | ("failure",_) => raise error "sys-error";
    1.26 +	      | ("failure",_) => error "sys-error";
    1.27  	val (_, ts) = 
    1.28  (* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]);
    1.29     *)
    1.30  	    (case step p ((pt, e_pos'),[]) of
    1.31  		 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
    1.32  	       | ("helpless",_) => ("helpless: cannot propose tac", [])
    1.33 -	       | ("no-fmz-spec",_) => raise error "no-fmz-spec"
    1.34 +	       | ("no-fmz-spec",_) => error "no-fmz-spec"
    1.35  	       | ("end-of-calculation", (ts, _, _)) => ("",ts))
    1.36 -	    handle _ => raise error "sys-error";
    1.37 +	    handle _ => error "sys-error";
    1.38  	val tac = case ts of tacis as (_::_) =>
    1.39  (* val tacis as (_::_) = ts;
    1.40     *)