1.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  fun to_string tacis = (strs2str o (map (linefeed o taci2str))) tacis
     1.5  fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
     1.6    | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
     1.7 -  | result (_, tac_, _) = error ("result: called with" ^ Tactic.string_of tac_)
     1.8 +  | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_)
     1.9  
    1.10  fun make_single ro erls (t, r as Rule.Thm (id, thm), (t', a)) = 
    1.11        (Tactic.Rewrite (id, thm), 
    1.12 @@ -61,7 +61,7 @@
    1.13        (Tactic.Rewrite_Set (Rule_Set.id_from_rule r), 
    1.14          Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
    1.15         (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    1.16 -  | make_single _ _ (t, r, _) = error ("make_single: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
    1.17 +  | make_single _ _ (t, r, _) = raise ERROR ("make_single: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
    1.18  
    1.19  (* update pos in tacis for embedding by generate *)
    1.20  fun insert_pos (_: Pos.pos) [] = []