diff -r 95d956108461 -r 460c24a6a6ba src/Tools/isac/Interpret/generate.sml
--- a/src/Tools/isac/Interpret/generate.sml	Tue Sep 28 08:58:06 2010 +0200
+++ b/src/Tools/isac/Interpret/generate.sml	Tue Sep 28 09:06:56 2010 +0200
@@ -12,14 +12,14 @@
 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
    *)
        | Rls {scr=EmptyScr,...} => 
-	 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
+	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
 		      ^"use prep_rls for storing rule-sets !")
        | Rls {scr=Script s,...} =>
 (* val Rls {scr=Script s,...} = assoc_rls rls;
    *)
 	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
        | Seq {scr=EmptyScr,...} => 
-	 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
+	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
 		      ^"use prep_rls for storing rule-sets !")
        | Seq {srls=srls,scr=Script s,...} =>
 	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
@@ -29,13 +29,13 @@
     let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
     in case assoc_rls rls of
            Rls {scr=EmptyScr,...} => 
-	   raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
+	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
 			^"use prep_rls for storing rule-sets !")
 	 | Rls {scr=Script s,...} =>
 	   let val (a1, a2) = two_scr_arg s
 	   in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
 	 | Seq {scr=EmptyScr,...} => 
-	   raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
+	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
 			^"use prep_rls for storing rule-sets !")
 (* val Seq {scr=Script s,...} = assoc_rls rls;
    *)
@@ -53,14 +53,14 @@
 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
    *)
        | Rls {scr=EmptyScr,...} => 
-	 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
+	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
 		      ^"use prep_rls for storing rule-sets !")
        | Rls {scr=Script s,...} =>
 (* val Rls {scr=Script s,...} = assoc_rls rls;
    *)
 	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
        | Seq {scr=EmptyScr,...} => 
-	 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
+	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
 		      ^"use prep_rls for storing rule-sets !")
        | Seq {srls=srls,scr=Script s,...} =>
 	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
@@ -71,14 +71,14 @@
     (*...we suppose the substitution of only _one_ bound variable*)
     in case assoc_rls rls of
            Rls {scr=EmptyScr,...} => 
-	   raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
+	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
 			^"use prep_rls for storing rule-sets !")
 	 | Rls {scr=Script s,...} =>
 	   let val (form, bdv) = two_scr_arg s
 	   in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
 	   end
 	 | Seq {scr=EmptyScr,...} => 
-	   raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
+	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
 			^"use prep_rls for storing rule-sets !")
 (* val Seq {scr=Script s,...} = assoc_rls rls;
    *)
@@ -482,14 +482,14 @@
     in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
 
   | generate1 thy m' _ _ _ = 
-    raise error ("generate1: not impl.for "^(tac_2str m'))
+    error ("generate1: not impl.for "^(tac_2str m'))
 ;
 
 
 fun generate_hard thy m' (p,p_) pt =
   let  
     val p = case p_ of Frm => p | Res => lev_on p
-  | _ => raise error ("generate_hard: call by "^(pos'2str (p,p_)));
+  | _ => error ("generate_hard: call by "^(pos'2str (p,p_)));
   in generate1 thy m' e_istate (p,p_) pt end;
 
 
@@ -539,7 +539,7 @@
 fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm)
   | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm)
   | res_from_taci (_, tac_, _) = 
-    raise error ("res_from_taci: called with" ^ tac_2str tac_);
+    error ("res_from_taci: called with" ^ tac_2str tac_);
 
 (*.embed the tacis created by a '_deriv'ation; sys.form <> input.form
   tacis are in order, thus are reverted for generate.*)