1.1 --- a/src/Tools/isac/Interpret/generate.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -12,14 +12,14 @@
     1.4  (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
     1.5     *)
     1.6         | Rls {scr=EmptyScr,...} => 
     1.7 -	 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
     1.8 +	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
     1.9  		      ^"use prep_rls for storing rule-sets !")
    1.10         | Rls {scr=Script s,...} =>
    1.11  (* val Rls {scr=Script s,...} = assoc_rls rls;
    1.12     *)
    1.13  	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
    1.14         | Seq {scr=EmptyScr,...} => 
    1.15 -	 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.16 +	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.17  		      ^"use prep_rls for storing rule-sets !")
    1.18         | Seq {srls=srls,scr=Script s,...} =>
    1.19  	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
    1.20 @@ -29,13 +29,13 @@
    1.21      let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
    1.22      in case assoc_rls rls of
    1.23             Rls {scr=EmptyScr,...} => 
    1.24 -	   raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.25 +	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.26  			^"use prep_rls for storing rule-sets !")
    1.27  	 | Rls {scr=Script s,...} =>
    1.28  	   let val (a1, a2) = two_scr_arg s
    1.29  	   in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
    1.30  	 | Seq {scr=EmptyScr,...} => 
    1.31 -	   raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.32 +	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.33  			^"use prep_rls for storing rule-sets !")
    1.34  (* val Seq {scr=Script s,...} = assoc_rls rls;
    1.35     *)
    1.36 @@ -53,14 +53,14 @@
    1.37  (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
    1.38     *)
    1.39         | Rls {scr=EmptyScr,...} => 
    1.40 -	 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.41 +	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.42  		      ^"use prep_rls for storing rule-sets !")
    1.43         | Rls {scr=Script s,...} =>
    1.44  (* val Rls {scr=Script s,...} = assoc_rls rls;
    1.45     *)
    1.46  	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
    1.47         | Seq {scr=EmptyScr,...} => 
    1.48 -	 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.49 +	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.50  		      ^"use prep_rls for storing rule-sets !")
    1.51         | Seq {srls=srls,scr=Script s,...} =>
    1.52  	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
    1.53 @@ -71,14 +71,14 @@
    1.54      (*...we suppose the substitution of only _one_ bound variable*)
    1.55      in case assoc_rls rls of
    1.56             Rls {scr=EmptyScr,...} => 
    1.57 -	   raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.58 +	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.59  			^"use prep_rls for storing rule-sets !")
    1.60  	 | Rls {scr=Script s,...} =>
    1.61  	   let val (form, bdv) = two_scr_arg s
    1.62  	   in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
    1.63  	   end
    1.64  	 | Seq {scr=EmptyScr,...} => 
    1.65 -	   raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.66 +	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.67  			^"use prep_rls for storing rule-sets !")
    1.68  (* val Seq {scr=Script s,...} = assoc_rls rls;
    1.69     *)
    1.70 @@ -482,14 +482,14 @@
    1.71      in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
    1.72  
    1.73    | generate1 thy m' _ _ _ = 
    1.74 -    raise error ("generate1: not impl.for "^(tac_2str m'))
    1.75 +    error ("generate1: not impl.for "^(tac_2str m'))
    1.76  ;
    1.77  
    1.78  
    1.79  fun generate_hard thy m' (p,p_) pt =
    1.80    let  
    1.81      val p = case p_ of Frm => p | Res => lev_on p
    1.82 -  | _ => raise error ("generate_hard: call by "^(pos'2str (p,p_)));
    1.83 +  | _ => error ("generate_hard: call by "^(pos'2str (p,p_)));
    1.84    in generate1 thy m' e_istate (p,p_) pt end;
    1.85  
    1.86  
    1.87 @@ -539,7 +539,7 @@
    1.88  fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm)
    1.89    | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm)
    1.90    | res_from_taci (_, tac_, _) = 
    1.91 -    raise error ("res_from_taci: called with" ^ tac_2str tac_);
    1.92 +    error ("res_from_taci: called with" ^ tac_2str tac_);
    1.93  
    1.94  (*.embed the tacis created by a '_deriv'ation; sys.form <> input.form
    1.95    tacis are in order, thus are reverted for generate.*)