1.1 --- a/src/Tools/isac/Test_Code/test-code.sml	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/Test_Code/test-code.sml	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -44,12 +44,12 @@
     1.4        Test_Out.PpcKF (
     1.5          (case p_ of Pos.Pbl => Test_Out.Problem []
     1.6            | Pos.Met => Test_Out.Method []
     1.7 -          | _ => error "TESTg_form: uncovered case",
     1.8 +          | _ => raise ERROR "TESTg_form: uncovered case",
     1.9   			Specify.itms2itemppc (ThyC.get_theory"Isac_Knowledge") gfr pre))
    1.10     end
    1.11  (* for quick test-print-out, until 'type inout' is removed *)
    1.12  fun f2str (Test_Out.FormKF cterm') = cterm'
    1.13 -  | f2str _ = error "f2str: uncovered case in fun.def.";                           
    1.14 +  | f2str _ = raise ERROR "f2str: uncovered case in fun.def.";                           
    1.15  
    1.16  (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
    1.17     compare "fun CalcTree" which DOES decode                        *)
    1.18 @@ -59,7 +59,7 @@
    1.19  	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
    1.20  	  val f = TESTg_form (pt,p)
    1.21    in (p, []:NEW, f, tac, Celem.Sundef, pt) end
    1.22 -| CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
    1.23 +| CalcTreeTEST _ = raise ERROR "CalcTreeTEST: uncovered case"
    1.24         
    1.25  fun me (*(Empty_Tac) p _ _ = raise ERROR ("me:  Empty_Tac at " ^ pos'2str p)
    1.26    | me*) tac p _(*NEW remove*) pt =
    1.27 @@ -71,8 +71,8 @@
    1.28    	    | ("unsafe-ok", (_, _, ptp)) => ptp
    1.29    	    | ("not-applicable",_) => (pt, p)
    1.30    	    | ("end-of-calculation", (_, _, ptp)) => ptp
    1.31 -  	    | ("failure", _) => error "sys-error"
    1.32 -  	    | _ => error "me: uncovered case Step.by_tactic"
    1.33 +  	    | ("failure", _) => raise ERROR "sys-raise ERROR"
    1.34 +  	    | _ => raise ERROR "me: uncovered case Step.by_tactic"
    1.35    	  val (_, ts) =
    1.36          (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
    1.37    	    (case Step.do_next p ((pt, Pos.e_pos'), []) of
    1.38 @@ -80,7 +80,7 @@
    1.39    	    | ("helpless", _) => ("helpless: cannot propose tac", [])
    1.40    	    | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*)
    1.41    	    | ("end-of-calculation", (ts, _, _)) => ("", ts)
    1.42 -  	    | _ => error  "me: uncovered case do_next")
    1.43 +  	    | _ => raise ERROR  "me: uncovered case do_next")
    1.44    	  val tac = 
    1.45          case ts of 
    1.46            tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 
    1.47 @@ -139,8 +139,8 @@
    1.48    	    | ("unsafe-ok", (_, _, ptp)) => ptp
    1.49    	    | ("not-applicable",_) => (pt, p)
    1.50    	    | ("end-of-calculation", (_, _, ptp)) => ptp
    1.51 -  	    | ("failure", _) => error "sys-error"
    1.52 -  	    | _ => error "me: uncovered case Step.by_tactic"
    1.53 +  	    | ("failure", _) => raise ERROR "sys-raise ERROR"
    1.54 +  	    | _ => raise ERROR "me: uncovered case Step.by_tactic"
    1.55        val _ = trace (pt', p') tac
    1.56    	  val (_, ts, (pt'', p'')) =
    1.57          (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
    1.58 @@ -149,7 +149,7 @@
    1.59    	    | ("helpless", _) => ("helpless: cannot propose tac", [], Ctree.e_state)
    1.60    	    | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts, Ctree.e_state) (*intermed.from specify*)
    1.61    	    | ("end-of-calculation", (ts, _, _)) => ("", ts, Ctree.e_state)
    1.62 -  	    | _ => error  "me: uncovered case do_next")
    1.63 +  	    | _ => raise ERROR  "me: uncovered case do_next")
    1.64    	  val tac'' = 
    1.65          case ts of 
    1.66            tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 
    1.67 @@ -164,6 +164,6 @@
    1.68  fun tac2tac_ pt p m = 
    1.69    case Step.check m (pt, p) of
    1.70  	  Applicable.Yes m' => m' 
    1.71 -  | Applicable.No _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m);
    1.72 +  | Applicable.No _ => raise ERROR ("tac2mstp': fails with" ^ Tactic.input_to_string m);
    1.73  
    1.74  (**)end(**)