1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -236,7 +236,7 @@
     1.4  
     1.5  fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
     1.6    | rls_of (Rewrite_Set rls) = rls
     1.7 -  | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
     1.8 +  | rls_of input = raise ERROR ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
     1.9  
    1.10  fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID)
    1.11    | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
    1.12 @@ -246,7 +246,7 @@
    1.13    | rule2tac _ subst (Rule.Rls_ rls) = 
    1.14      Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls))
    1.15    | rule2tac _ _ rule = 
    1.16 -    error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
    1.17 +    raise ERROR ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
    1.18  
    1.19  (* try if a rewrite-rule is applicable to a given formula; 
    1.20     in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 
    1.21 @@ -267,13 +267,13 @@
    1.22  	      SOME _ => [rule2tac thy [] cal]
    1.23        | NONE => [])
    1.24    | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
    1.25 -  | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
    1.26 +  | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case"
    1.27  and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) = 
    1.28      gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
    1.29    | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) = 
    1.30      gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
    1.31    | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
    1.32 -  | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
    1.33 +  | filter_appl_rews _ _ _ _ = raise ERROR "filter_appl_rews: uncovered case"
    1.34  
    1.35  (* decide if a tactic is applicable to a given formula; 
    1.36     in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)