1.1 --- a/src/Tools/isac/Specify/refine.sml	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4        | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
     1.5    | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
     1.6        (case find_first (eq1 d) pbt of
     1.7 -        SOME (_, _) => error "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, I_Model.pbl_ids' d vs))):itm)"
     1.8 +        SOME (_, _) => raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, I_Model.pbl_ids' d vs))):itm)"
     1.9        | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
    1.10    | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
    1.11  
    1.12 @@ -110,7 +110,7 @@
    1.13  	    in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
    1.14         else (pbls @ [NoMatch_])
    1.15      end
    1.16 -  | refin'' _ _ _ _ _ = error "refin': uncovered fun def."
    1.17 +  | refin'' _ _ _ _ _ = raise ERROR "refin': uncovered fun def."
    1.18  and refins'' _ _ _ pbls [] = pbls
    1.19    | refins'' thy pblRD itms pbls ((p as Store.Node _) :: pts) =
    1.20      let