1.1 --- a/src/Tools/isac/Interpret/ctree.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -303,7 +303,7 @@
     1.4  
     1.5  fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
     1.6      (ScrState (env, loc_, topt, v, safe, bool))
     1.7 -  | new_val _ _ = raise error "new_val: only for ScrState";
     1.8 +  | new_val _ _ = error "new_val: only for ScrState";
     1.9  
    1.10  datatype con = land | lor;
    1.11  
    1.12 @@ -500,7 +500,7 @@
    1.13  
    1.14  fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
    1.15    | rls_of (Rewrite_Set rls) = rls
    1.16 -  | rls_of tac = raise error ("rls_of: called with tac '"^tac2IDstr tac^"'");
    1.17 +  | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'");
    1.18  
    1.19  fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = 
    1.20      (thmID, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst))
    1.21 @@ -522,7 +522,7 @@
    1.22    | rule2tac subst (Rls_ rls) = 
    1.23      Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
    1.24    | rule2tac _ rule = 
    1.25 -    raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");
    1.26 +    error ("rule2tac: called with '" ^ rule2str rule ^ "'");
    1.27  
    1.28  type fmz_ = cterm' list;
    1.29  
    1.30 @@ -834,7 +834,7 @@
    1.31  
    1.32  (*4.4.00*)
    1.33  fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos'
    1.34 -  | lev_up_ p' = raise error ("lev_up_: called for "^(pos'2str p'));
    1.35 +  | lev_up_ p' = error ("lev_up_: called for "^(pos'2str p'));
    1.36  fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos'
    1.37  fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*)
    1.38  fun lev_of ((p,_):pos') = length p;
    1.39 @@ -1478,17 +1478,17 @@
    1.40  fun get_somespec ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
    1.41      let val domID = if dI = e_domID
    1.42  		    then if dI' = e_domID 
    1.43 -			 then raise error"pt_extract: no domID in probl,origin"
    1.44 +			 then error"pt_extract: no domID in probl,origin"
    1.45  			 else dI'
    1.46  		    else dI
    1.47  	val pblID = if pI = e_pblID
    1.48  		    then if pI' = e_pblID 
    1.49 -			 then raise error"pt_extract: no pblID in probl,origin"
    1.50 +			 then error"pt_extract: no pblID in probl,origin"
    1.51  			 else pI'
    1.52  		    else pI
    1.53  	val metID = if mI = e_metID
    1.54  		    then if pI' = e_metID 
    1.55 -			 then raise error"pt_extract: no metID in probl,origin"
    1.56 +			 then error"pt_extract: no metID in probl,origin"
    1.57  			 else mI'
    1.58  		    else mI
    1.59      in (domID, pblID, metID):spec end;
    1.60 @@ -1735,12 +1735,12 @@
    1.61    | lev_on' pt (p, Res) =
    1.62      if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*)
    1.63      then if existpt' (lev_on p, Res) pt then (lev_on p, Res)
    1.64 -	 else raise error ("lev_on': (p, Res) -> (p, Res) not existent, \
    1.65 +	 else error ("lev_on': (p, Res) -> (p, Res) not existent, \
    1.66  		      \p = "^ints2str' (lev_on p))
    1.67      else (lev_on p, Frm)
    1.68    | lev_on' pt (p, _) =
    1.69      if existpt' (p, Res) pt then (p, Res)
    1.70 -    else raise error ("lev_on': (p, Frm) -> (p, Res) not existent, \
    1.71 +    else error ("lev_on': (p, Frm) -> (p, Res) not existent, \
    1.72  		      \p = "^ints2str' p);
    1.73  
    1.74  fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false;
    1.75 @@ -2150,5 +2150,5 @@
    1.76  (*.get the theory explicitly specified for the rootpbl;
    1.77     thus use this function _after_ finishing specification.*)
    1.78  fun rootthy (Nd (PblObj {spec=(thyID, _, _),...}, _)) = assoc_thy thyID
    1.79 -  | rootthy _ = raise error "rootthy";
    1.80 +  | rootthy _ = error "rootthy";
    1.81