1.1 --- a/src/Tools/isac/Interpret/mstools.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/mstools.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -210,7 +210,7 @@
1.4 (theory "Isac")
1.5 (*comp_dts:FIXXME stay with term for efficiency !!*)
1.6 (d $ (comp_ts (d, ts)))
1.7 - handle _ => raise error ("comp_dts: "^(term2str d)^
1.8 + handle _ => error ("comp_dts: "^(term2str d)^
1.9 " $ "^(term2str (hd ts))));*)
1.10 fun comp_dts thy (d,[]) =
1.11 (if is_reall_dsc d then (d $ e_listReal)
1.12 @@ -218,7 +218,7 @@
1.13 else d)
1.14 | comp_dts thy (d,ts) =
1.15 (d $ (comp_ts (d, ts)))
1.16 - handle _ => raise error ("comp_dts: "^(term2str d)^
1.17 + handle _ => error ("comp_dts: "^(term2str d)^
1.18 " $ "^(term2str (hd ts)));
1.19 (*25.8.03*)
1.20 fun comp_dts' (d,[]) =
1.21 @@ -226,7 +226,7 @@
1.22 else if is_booll_dsc d then (d $ e_listBool)
1.23 else d
1.24 | comp_dts' (d,ts) = (d $ (comp_ts (d, ts)))
1.25 - handle _ => raise error ("comp_dts': "^(term2str d)^
1.26 + handle _ => error ("comp_dts': "^(term2str d)^
1.27 " $ "^(term2str (hd ts)));
1.28 (*val t = str2term "maximum A";
1.29 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.30 @@ -288,7 +288,7 @@
1.31 else if is_booll_dsc d then term2str (d $ e_listBool)
1.32 else term2str d
1.33 | comp_dts'' (d,ts) = term2str (d $ (comp_ts (d, ts)))
1.34 - handle _ => raise error ("comp_dts'': "^(term2str d)^
1.35 + handle _ => error ("comp_dts'': "^(term2str d)^
1.36 " $ "^(term2str (hd ts)));
1.37
1.38
1.39 @@ -387,7 +387,7 @@
1.40
1.41 (*. 14.9.01: not used after putting penv-values into itm_
1.42 make the result of split_* a value of problem-environment .*)
1.43 -fun mkval dsc [] = raise error "mkval called with []"
1.44 +fun mkval dsc [] = error "mkval called with []"
1.45 | mkval dsc [t] = t
1.46 | mkval dsc ts = list2isalist ((type_of o hd) ts) ts;
1.47 (*WN.12.12.03*)
1.48 @@ -398,7 +398,7 @@
1.49 (*. get the constant value from a penv .*)
1.50 fun getval (id, values) =
1.51 case values of
1.52 - [] => raise error ("penv_value: no values in '"^
1.53 + [] => error ("penv_value: no values in '"^
1.54 (Syntax.string_of_term (thy2ctxt' "Tools") id))
1.55 | [v] => (id, v)
1.56 | (v1::v2::_) => (case v1 of
1.57 @@ -523,7 +523,7 @@
1.58 fun cnt itms v = (v,(length o (filter (curry op= v)) o
1.59 flat o (map #2)) (itms:itm list));
1.60 fun vts_cnt vts itms = map (cnt itms) vts;
1.61 -fun max2 [] = raise error "max2 of []"
1.62 +fun max2 [] = error "max2 of []"
1.63 | max2 (y::ys) =
1.64 let fun mx (a,x) [] = (a,x)
1.65 | mx (a,x) ((b,y)::ys) =
1.66 @@ -594,7 +594,7 @@
1.67 then [v] (*eg. [r=Arbfix]*)
1.68 else (case v of (*eg. eps=#0*)
1.69 (Const ("op =",_) $ l $ r) => [r,l]
1.70 - | _ => raise error ("pbl_ids Tools.nam: no equality "
1.71 + | _ => error ("pbl_ids Tools.nam: no equality "
1.72 ^(Syntax.string_of_term ctxt v)))
1.73 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
1.74 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
1.75 @@ -602,7 +602,7 @@
1.76 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v]
1.77 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v]
1.78 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v]
1.79 - | pbl_ids ctxt _ v = raise error ("pbl_ids: not implemented for "
1.80 + | pbl_ids ctxt _ v = error ("pbl_ids: not implemented for "
1.81 ^(Syntax.string_of_term ctxt v));
1.82 (*
1.83 val t as t1 $ t2 = str2term "antiDerivativeName M_b";
1.84 @@ -637,10 +637,10 @@
1.85 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
1.86 fun pbl_ids' (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) vs =
1.87 (case vs of
1.88 - [] => raise error ("pbl_ids' Tools.nam called with []")
1.89 + [] => error ("pbl_ids' Tools.nam called with []")
1.90 | [t] => (case t of (*eg. eps=#0*)
1.91 (Const ("op =",_) $ l $ r) => [r,l]
1.92 - | _ => raise error ("pbl_ids' Tools.nam: no equality "
1.93 + | _ => error ("pbl_ids' Tools.nam: no equality "
1.94 ^(Syntax.string_of_term (thy2ctxt' "Isac")t)))
1.95 | vs' => vs (*14.9.01: ???TODO *))
1.96 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs
1.97 @@ -650,7 +650,7 @@
1.98 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))vs = vs
1.99 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))vs = vs
1.100 | pbl_ids' _ vs =
1.101 - raise error ("pbl_ids': not implemented for "
1.102 + error ("pbl_ids': not implemented for "
1.103 ^(terms2str vs));
1.104 (*9.5.03 penv postponed: pbl_ids'*)
1.105 fun pbl_ids' thy d vs = [comp_ts (d, vs)];