1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4              else chk (indets @ [t] @ a') asms);
     1.5        in chk [] asms end
     1.6  and rewrite__set_ thy _ __ Rule_Set.Empty t =                             (* rewrite with a rule set *)
     1.7 -    error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
     1.8 +    raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
     1.9    | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t =      (* rewrite with a 'reverse rule set' *)
    1.10      let
    1.11        val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
    1.12 @@ -165,7 +165,7 @@
    1.13                  let 
    1.14                    val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
    1.15                      ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
    1.16 -                  val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ 
    1.17 +                  val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^ 
    1.18                      ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
    1.19                    val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
    1.20                  in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
    1.21 @@ -179,7 +179,7 @@
    1.22                  let 
    1.23                    val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
    1.24                      ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
    1.25 -                  val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
    1.26 +                  val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
    1.27                       ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
    1.28                    val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
    1.29                  in the pairopt end
    1.30 @@ -280,7 +280,7 @@
    1.31           SOME (rew, _) => rew
    1.32         | NONE => raise ERROR ""
    1.33       in SOME (rew, (thmID, thm)) end)
    1.34 -	   handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
    1.35 +	   handle _ (*TODO Pattern.MATCH ?del?*)=> raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite")
    1.36    end;
    1.37  
    1.38  fun eval_prog_expr thy srls t =