1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4    in chk [] asms end
     1.5  (* rewrite with a rule set, which must not be the empty Erls *)
     1.6  and rewrite__set_ _ _ __ Erls t = 
     1.7 -    raise error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
     1.8 +    error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
     1.9    (* rewrite with a 'reverse rule set' based on ML code *)
    1.10    | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
    1.11      let val _= if ! trace_rewrite andalso i < ! depth 
    1.12 @@ -141,7 +141,7 @@
    1.13  		   rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
    1.14  		   ((#erls o rep_rls) rls) put_asm thm' ct;
    1.15  		 val _ = if pairopt <> NONE then () 
    1.16 -			 else raise error("rewrite_set_, rewrite_ \""^
    1.17 +			 else error("rewrite_set_, rewrite_ \""^
    1.18  			 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
    1.19  		 val _ = if ! trace_rewrite andalso i < ! depth 
    1.20  			   then tracing((idt"="(i+1))^" calc. to: "^
    1.21 @@ -161,7 +161,7 @@
    1.22  		   rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
    1.23  		   ((#erls o rep_rls) rls) put_asm thm' ct;
    1.24  		 val _ = if pairopt <> NONE then () 
    1.25 -			 else raise error("rewrite_set_, rewrite_ \""^
    1.26 +			 else error("rewrite_set_, rewrite_ \""^
    1.27  			 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
    1.28  		 val _ = if ! trace_rewrite andalso i < ! depth 
    1.29  			   then tracing((idt"="(i+1))^" cal1. to: "^
    1.30 @@ -333,7 +333,7 @@
    1.31  
    1.32  
    1.33  fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs'))
    1.34 -  handle _ => raise error ("get_rls_scr: no script for "^rs');
    1.35 +  handle _ => error ("get_rls_scr: no script for "^rs');
    1.36  
    1.37  
    1.38  (*make_thm added to Pure/thm.ML*)
    1.39 @@ -415,7 +415,7 @@
    1.40  	then mk_thm thy ct'
    1.41  	else (num_str o (PureThy.get_thm thy)) thmid
    1.42  	     ) handle _ => 
    1.43 -		      raise error ("assoc_thm': '"^thmid^"' not in '"^
    1.44 +		      error ("assoc_thm': '"^thmid^"' not in '"^
    1.45  				   (theory2domID thy)^"' (and parents)");
    1.46  (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3");
    1.47  val it = "6 = 2 * 3" : thm