1.1 --- a/src/Tools/isac/Interpret/appl.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -13,7 +13,7 @@
1.4 (rew_ord',erls,ca)
1.5 | rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
1.6 (rew_ord',erls, ca)
1.7 - | rew_info rls = raise error ("rew_info called with '"^rls2str rls^"'");
1.8 + | rew_info rls = error ("rew_info called with '"^rls2str rls^"'");
1.9
1.10 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
1.11 fun from_pblobj_or_detail_thm thm' p pt =
1.12 @@ -107,7 +107,7 @@
1.13 in (bdv, pred) end
1.14
1.15 | mk_set thy _ _ l _ =
1.16 - raise error ("check_elementwise: no set "^
1.17 + error ("check_elementwise: no set "^
1.18 (Syntax.string_of_term (thy2ctxt thy) l));
1.19 (*> val consts = str2term "[x=#4]";
1.20 > val pred = str2term "Assumptions";
1.21 @@ -373,7 +373,7 @@
1.22 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.23 Frm => (get_obj g_form pt p, p)
1.24 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.25 - | _ => raise error ("applicable_in: call by "^
1.26 + | _ => error ("applicable_in: call by "^
1.27 (pos'2str (p,p_)));
1.28 in
1.29 let val subst = subs2subst thy subs;
1.30 @@ -400,7 +400,7 @@
1.31 val f = case p_ of
1.32 Frm => get_obj g_form pt p
1.33 | Res => (fst o (get_obj g_result pt)) p
1.34 - | _ => raise error ("applicable_in Rewrite: call by "^
1.35 + | _ => error ("applicable_in Rewrite: call by "^
1.36 (pos'2str (p,p_)));
1.37 in if msg = "OK"
1.38 then
1.39 @@ -429,7 +429,7 @@
1.40 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.41 Frm => (get_obj g_form pt p, p)
1.42 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.43 - | _ => raise error ("applicable_in: call by "^
1.44 + | _ => error ("applicable_in: call by "^
1.45 (pos'2str (p,p_)));
1.46 in case rewrite_ thy (assoc_rew_ord ro') erls
1.47 (*put_asm*)false (assoc_thm' thy thm') f of
1.48 @@ -448,7 +448,7 @@
1.49 val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);
1.50 val f = case p_ of Frm => get_obj g_form pt p
1.51 | Res => (fst o (get_obj g_result pt)) p
1.52 - | _ => raise error ("applicable_in: call by "^
1.53 + | _ => error ("applicable_in: call by "^
1.54 (pos'2str (p,p_)));
1.55 in
1.56 let val subst = subs2subst thy subs
1.57 @@ -472,7 +472,7 @@
1.58 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.59 Frm => (get_obj g_form pt p, p)
1.60 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.61 - | _ => raise error ("applicable_in: call by "^
1.62 + | _ => error ("applicable_in: call by "^
1.63 (pos'2str (p,p_)));
1.64 in
1.65 let val subst = subs2subst thy subs;
1.66 @@ -493,7 +493,7 @@
1.67 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.68 Frm => (get_obj g_form pt p, p)
1.69 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.70 - | _ => raise error ("applicable_in: call by "^
1.71 + | _ => error ("applicable_in: call by "^
1.72 (pos'2str (p,p_)));
1.73 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
1.74 SOME (f',asm) =>
1.75 @@ -511,7 +511,7 @@
1.76 val f = case p_ of
1.77 Frm => get_obj g_form pt p
1.78 | Res => (fst o (get_obj g_result pt)) p
1.79 - | _ => raise error ("applicable_in: call by "^
1.80 + | _ => error ("applicable_in: call by "^
1.81 (pos'2str (p,p_)));
1.82 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
1.83 SOME (f',asm) =>
1.84 @@ -520,7 +520,7 @@
1.85
1.86
1.87 | applicable_in p pt (End_Ruleset) =
1.88 - raise error ("applicable_in: not impl. for "^
1.89 + error ("applicable_in: not impl. for "^
1.90 (tac2str End_Ruleset))
1.91
1.92 (* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);
1.93 @@ -587,7 +587,7 @@
1.94 ------------------*)
1.95
1.96 | applicable_in p pt (Apply_Assumption cts') =
1.97 - (raise error ("applicable_in: not impl. for "^
1.98 + (error ("applicable_in: not impl. for "^
1.99 (tac2str (Apply_Assumption cts'))))
1.100
1.101 (*'logical' applicability wrt. script in locate: Inconsistent?*)
1.102 @@ -602,11 +602,11 @@
1.103 end
1.104
1.105 | applicable_in p pt (Take_Inst ct') =
1.106 - raise error ("applicable_in: not impl. for "^
1.107 + error ("applicable_in: not impl. for "^
1.108 (tac2str (Take_Inst ct')))
1.109
1.110 | applicable_in p pt (Group (con, ints)) =
1.111 - raise error ("applicable_in: not impl. for "^
1.112 + error ("applicable_in: not impl. for "^
1.113 (tac2str (Group (con, ints))))
1.114
1.115 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
1.116 @@ -621,24 +621,24 @@
1.117 e_term, [], subpbl domID pblID))
1.118
1.119 | applicable_in p pt (End_Subproblem) =
1.120 - raise error ("applicable_in: not impl. for "^
1.121 + error ("applicable_in: not impl. for "^
1.122 (tac2str (End_Subproblem)))
1.123
1.124 | applicable_in p pt (CAScmd ct') =
1.125 - raise error ("applicable_in: not impl. for "^
1.126 + error ("applicable_in: not impl. for "^
1.127 (tac2str (CAScmd ct')))
1.128
1.129 | applicable_in p pt (Split_And) =
1.130 - raise error ("applicable_in: not impl. for "^
1.131 + error ("applicable_in: not impl. for "^
1.132 (tac2str (Split_And)))
1.133 | applicable_in p pt (Conclude_And) =
1.134 - raise error ("applicable_in: not impl. for "^
1.135 + error ("applicable_in: not impl. for "^
1.136 (tac2str (Conclude_And)))
1.137 | applicable_in p pt (Split_Or) =
1.138 - raise error ("applicable_in: not impl. for "^
1.139 + error ("applicable_in: not impl. for "^
1.140 (tac2str (Split_Or)))
1.141 | applicable_in p pt (Conclude_Or) =
1.142 - raise error ("applicable_in: not impl. for "^
1.143 + error ("applicable_in: not impl. for "^
1.144 (tac2str (Conclude_Or)))
1.145
1.146 | applicable_in (p,p_) pt (Begin_Trans) =
1.147 @@ -647,11 +647,11 @@
1.148 (*_____ implizit Take in gen*)
1.149 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
1.150 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
1.151 - | _ => raise error ("applicable_in: call by "^
1.152 + | _ => error ("applicable_in: call by "^
1.153 (pos'2str (p,p_)));
1.154 val thy' = get_obj g_domID pt (par_pblobj pt p);
1.155 in (Appl (Begin_Trans' f))
1.156 - handle _ => raise error ("applicable_in: Begin_Trans finds \
1.157 + handle _ => error ("applicable_in: Begin_Trans finds \
1.158 \syntaxerror in '"^(term2str f)^"'") end
1.159
1.160 (*TODO: check parent branches*)
1.161 @@ -665,16 +665,16 @@
1.162 end
1.163
1.164 | applicable_in p pt (Begin_Sequ) =
1.165 - raise error ("applicable_in: not impl. for "^
1.166 + error ("applicable_in: not impl. for "^
1.167 (tac2str (Begin_Sequ)))
1.168 | applicable_in p pt (End_Sequ) =
1.169 - raise error ("applicable_in: not impl. for "^
1.170 + error ("applicable_in: not impl. for "^
1.171 (tac2str (End_Sequ)))
1.172 | applicable_in p pt (Split_Intersect) =
1.173 - raise error ("applicable_in: not impl. for "^
1.174 + error ("applicable_in: not impl. for "^
1.175 (tac2str (Split_Intersect)))
1.176 | applicable_in p pt (End_Intersect) =
1.177 - raise error ("applicable_in: not impl. for "^
1.178 + error ("applicable_in: not impl. for "^
1.179 (tac2str (End_Intersect)))
1.180 (* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it;
1.181 val (vvv,ppp) = vp;
1.182 @@ -735,7 +735,7 @@
1.183 end
1.184
1.185 | applicable_in p pt (Collect_Trues) =
1.186 - raise error ("applicable_in: not impl. for "^
1.187 + error ("applicable_in: not impl. for "^
1.188 (tac2str (Collect_Trues)))
1.189
1.190 | applicable_in p pt (Empty_Tac) =
1.191 @@ -771,12 +771,12 @@
1.192 | applicable_in p pt End_Proof' = Appl End_Proof''
1.193
1.194 | applicable_in _ _ m =
1.195 - raise error ("applicable_in called for "^(tac2str m));
1.196 + error ("applicable_in called for "^(tac2str m));
1.197
1.198 (*WN060614 unused*)
1.199 fun tac2tac_ pt p m =
1.200 case applicable_in p pt m of
1.201 Appl (m') => m'
1.202 - | Notappl _ => raise error ("tac2mstp': fails with"^
1.203 + | Notappl _ => error ("tac2mstp': fails with"^
1.204 (tac2str m));
1.205