1.1 --- a/src/Tools/isac/Interpret/inform.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -252,7 +252,7 @@
     1.4       (*this    ^ should raise the exn on unability of re-parsing dts*)
     1.5       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
     1.6    | parsitm dI (itm as (i,v,_,f, Par _)) = 
     1.7 -    raise error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^
     1.8 +    error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^
     1.9  		 "): Par should be internal");
    1.10  
    1.11  (*separate a list to a pair of elements that do NOT satisfy the predicate,
    1.12 @@ -294,7 +294,7 @@
    1.13  	      ("",itm)  => itm
    1.14  	 (* val (msg,xx) = is_notyet_input thy ppc all ori' pbt;
    1.15  	    *)
    1.16 -	    | (msg,_) => raise error ("appl_add': "^msg))
    1.17 +	    | (msg,_) => error ("appl_add': "^msg))
    1.18  	 (* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct);
    1.19  	    *)
    1.20         | (msg,(i,v,_,d,ts),_) => 
    1.21 @@ -392,7 +392,7 @@
    1.22  
    1.23  
    1.24  fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
    1.25 -  | par2fstr itm = raise error ("par2fstr: called with " ^
    1.26 +  | par2fstr itm = error ("par2fstr: called with " ^
    1.27  			      itm2str_ (thy2ctxt' "Isac") itm);
    1.28  fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts))
    1.29    | itms2fstr (_,_,_,f, Syn str) = (f, str)
    1.30 @@ -401,7 +401,7 @@
    1.31    | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts))
    1.32    | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t))
    1.33    | itms2fstr (itm as (_,_,_,f, Par _)) = 
    1.34 -    raise error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^
    1.35 +    error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^
    1.36  		 "): Par should be internal");
    1.37  
    1.38  fun imodel2fstr iitems = 
    1.39 @@ -479,7 +479,7 @@
    1.40  		    Met, hdf', mits, pre, spec):ocalhd) end
    1.41         end end
    1.42    | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) =
    1.43 -    raise error "input_icalhd Met not impl.";
    1.44 +    error "input_icalhd Met not impl.";
    1.45  
    1.46  
    1.47  (***. handle an input formula .***)
    1.48 @@ -562,13 +562,13 @@
    1.49      if equal f1 i1 then
    1.50  	 if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is)
    1.51  	 else (rev (f1::f2::fs), i1::i2::is)
    1.52 -    else raise error "dropwhile': did not start with equal elements"
    1.53 +    else error "dropwhile': did not start with equal elements"
    1.54    | dropwhile' equal (f::fs) [i] =
    1.55      if equal f i then (rev (f::fs), [i])
    1.56 -    else raise error "dropwhile': did not start with equal elements"
    1.57 +    else error "dropwhile': did not start with equal elements"
    1.58    | dropwhile' equal [f] (i::is) =
    1.59      if equal f i then ([f], i::is)
    1.60 -    else raise error "dropwhile': did not start with equal elements";
    1.61 +    else error "dropwhile': did not start with equal elements";
    1.62  (*
    1.63   fun equal a b = a=b;
    1.64   val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];