1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -109,7 +109,7 @@
1.4 (case goal of
1.5 NONE => rts
1.6 | SOME g =>
1.7 - raise error ("make_deriv: no derivation for "^(term2str t)))
1.8 + error ("make_deriv: no derivation for "^(term2str t)))
1.9 | rew_once lim rts t Appl [] =
1.10 (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs
1.11 (*| Seq _ => rts) FIXXXXXME 14.3.03*)
1.12 @@ -147,7 +147,7 @@
1.13 val r' = Thm (thmid, tm)
1.14 in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
1.15 end)
1.16 - handle _ => raise error "derive_norm, Calc: no rewrite"
1.17 + handle _ => error "derive_norm, Calc: no rewrite"
1.18 end
1.19 (* TODO.WN080222: see rewrite__set_
1.20 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
1.21 @@ -163,7 +163,7 @@
1.22 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
1.23 ((#erls o rep_rls) rls) put_asm thm' ct;
1.24 val _ = if pairopt <> NONE then ()
1.25 - else raise error("rewrite_set_, rewrite_ \""^
1.26 + else error("rewrite_set_, rewrite_ \""^
1.27 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
1.28 val _ = if ! trace_rewrite andalso i < ! depth
1.29 then tracing((idt"="(i+1))^" cal1. to: "^
1.30 @@ -229,7 +229,7 @@
1.31
1.32 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)
1.33 | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
1.34 - | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));
1.35 + | sym_Thm r = error ("sym_Thm: not for "^(rule2str r));
1.36 (*
1.37 val th = Thm ("real_one_collect",num_str @{thm real_one_collect});
1.38 sym_Thm th;
1.39 @@ -255,7 +255,7 @@
1.40 | eq_Thm (Thm (id1,_), _) = false
1.41 | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2
1.42 | eq_Thm (Rls_ r1, _) = false
1.43 - | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^
1.44 + | eq_Thm (r1, r2) = error ("eq_Thm: called with '"^
1.45 (rule2str r1)^"' '"^(rule2str r2)^"'");
1.46 fun distinct_Thm r = gen_distinct eq_Thm r;
1.47
1.48 @@ -271,8 +271,8 @@
1.49 "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
1.50 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
1.51 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
1.52 - | str => raise error ("thy2guh: called with '"^str^"'"))
1.53 - | part2guh theID = raise error ("part2guh called with theID = "
1.54 + | str => error ("thy2guh: called with '"^str^"'"))
1.55 + | part2guh theID = error ("part2guh called with theID = "
1.56 ^ theID2str theID);
1.57 fun part2filename str = part2guh str ^ ".xml" : filename;
1.58
1.59 @@ -282,15 +282,15 @@
1.60 "Isabelle" => "thy_isab_" ^ thyID : guh
1.61 | "IsacScripts" => "thy_scri_" ^ thyID
1.62 | "IsacKnowledge" => "thy_isac_" ^ thyID
1.63 - | str => raise error ("thy2guh: called with '"^str^"'"))
1.64 - | thy2guh theID = raise error ("thy2guh called with '"^strs2str' theID^"'");
1.65 + | str => error ("thy2guh: called with '"^str^"'"))
1.66 + | thy2guh theID = error ("thy2guh called with '"^strs2str' theID^"'");
1.67 fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename;
1.68 fun thypart2guh ([part, thyID, thypart]:theID) =
1.69 case part of
1.70 "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
1.71 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
1.72 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
1.73 - | str => raise error ("thypart2guh: called with '"^str^"'");
1.74 + | str => error ("thypart2guh: called with '"^str^"'");
1.75 fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename;
1.76
1.77 (*.convert the data got via contextToThy to a globally unique handle
1.78 @@ -303,7 +303,7 @@
1.79 "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
1.80 | "IsacScripts" =>
1.81 "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
1.82 - | str => raise error ("thm2guh called with isa = '"^isa^
1.83 + | str => error ("thm2guh called with isa = '"^isa^
1.84 "' for thm = "^thmID^"'");
1.85 fun thm2filename (isa_thyID: string * thyID) thmID =
1.86 (thm2guh isa_thyID thmID) ^ ".xml" : filename;
1.87 @@ -316,7 +316,7 @@
1.88 "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
1.89 | "IsacScripts" =>
1.90 "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
1.91 - | str => raise error ("rls2guh called with isa = '"^isa^
1.92 + | str => error ("rls2guh called with isa = '"^isa^
1.93 "' for rls = '"^rls'^"'");
1.94 fun rls2filename (isa, thyID) rls' =
1.95 rls2guh (isa, thyID) rls' ^ ".xml" : filename;
1.96 @@ -329,7 +329,7 @@
1.97 "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
1.98 | "IsacScripts" =>
1.99 "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
1.100 - | str => raise error ("cal2guh called with isa = '"^isa^
1.101 + | str => error ("cal2guh called with isa = '"^isa^
1.102 "' for cal = '"^calID^"'");
1.103 fun cal2filename (isa, thyID:thyID) calID =
1.104 cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename;
1.105 @@ -342,7 +342,7 @@
1.106 "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
1.107 | "IsacScripts" =>
1.108 "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
1.109 - | str => raise error ("ord2guh called with isa = '"^isa^
1.110 + | str => error ("ord2guh called with isa = '"^isa^
1.111 "' for ord = '"^rew_ord'^"'");
1.112 fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') =
1.113 ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename;
1.114 @@ -421,7 +421,7 @@
1.115 | NONE => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of
1.116 SOME (thyID,_) => ("Isabelle", thyID)
1.117 | NONE =>
1.118 - raise error ("thy_containing_thm: theorem '"^str^
1.119 + error ("thy_containing_thm: theorem '"^str^
1.120 "' not in !theory' above thy '"^thy'^"'"))
1.121 end;
1.122
1.123 @@ -450,7 +450,7 @@
1.124 (rev (!ruleset'))
1.125 in case assoc (startsearch, rls') of
1.126 SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
1.127 - | _ => raise error ("thy_containing_rls : rls '"^rls'^
1.128 + | _ => error ("thy_containing_rls : rls '"^rls'^
1.129 "' not in !rulset' above thy '"^thy'^"'")
1.130 end;
1.131 (* val (thy', termop) = (thyID, termop);
1.132 @@ -466,7 +466,7 @@
1.133 (#1 : calc -> string)) (rev (!calclist'))
1.134 in case assoc (startsearch, strip_thy termop) of
1.135 SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
1.136 - | _ => raise error ("thy_containing_rls : rls '"^termop^
1.137 + | _ => error ("thy_containing_rls : rls '"^termop^
1.138 "' not in !calclist' above thy '"^thy'^"'")
1.139 end
1.140 end;
1.141 @@ -741,7 +741,7 @@
1.142 (*.not only for thydata, but also for thy's etc.*)
1.143 fun theID2guh (theID:theID) =
1.144 case length theID of
1.145 - 0 => raise error ("theID2guh: called with theID = "^strs2str' theID)
1.146 + 0 => error ("theID2guh: called with theID = "^strs2str' theID)
1.147 | 1 => part2guh theID
1.148 | 2 => thy2guh theID
1.149 | 3 => thypart2guh theID
1.150 @@ -752,10 +752,10 @@
1.151 | "Calculations" => cal2guh (isa, thyID) elemID
1.152 | "Orders" => ord2guh (isa, thyID) elemID
1.153 | "Theorems" => thy2guh [isa, thyID]
1.154 - | str => raise error ("theID2guh: called with theID = "^
1.155 + | str => error ("theID2guh: called with theID = "^
1.156 strs2str' theID)
1.157 end
1.158 - | n => raise error ("theID2guh called with theID = "^strs2str' theID);
1.159 + | n => error ("theID2guh called with theID = "^strs2str' theID);
1.160 (*.filenames not only for thydata, but also for thy's etc.*)
1.161 fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;
1.162
1.163 @@ -764,14 +764,14 @@
1.164 val part = implode (take_fromto 1 4 guh')
1.165 val isa = implode (take_fromto 5 9 guh')
1.166 in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
1.167 - then raise error ("guh '"^guh^"' does not begin with \
1.168 + then error ("guh '"^guh^"' does not begin with \
1.169 \exp_ | thy_ | pbl_ | met_")
1.170 else let val chap = case isa of
1.171 "isab_" => "Isabelle"
1.172 | "scri_" => "IsacScripts"
1.173 | "isac_" => "IsacKnowledge"
1.174 | _ =>
1.175 - raise error ("guh2theID: '"^guh^
1.176 + error ("guh2theID: '"^guh^
1.177 "' does not have isab_ | scri_ | \
1.178 \isac_ at position 5..9")
1.179 val rest = takerest (9, guh')
1.180 @@ -793,7 +793,7 @@
1.181 | "-cal-" => "Operations"
1.182 | "-ord-" => "Orders"
1.183 | str =>
1.184 - raise error ("guh2theID: '"^guh^"' has '"^sect^
1.185 + error ("guh2theID: '"^guh^"' has '"^sect^
1.186 "' instead -thm- | -rls- | \
1.187 \-cal- | -ord-")
1.188 in [chap, implode thyID, sect', implode
1.189 @@ -815,14 +815,14 @@
1.190 in case sect of
1.191 "Theorems" => Rewrite (xstr, "")
1.192 | "Rulesets" => Rewrite_Set xstr
1.193 - | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'")
1.194 + | str => error ("guh2rewtac: not impl. for '"^xstr^"'")
1.195 end
1.196 | guh2rewtac (guh:guh) subs =
1.197 let val [isa, thy, sect, xstr] = guh2theID guh
1.198 in case sect of
1.199 "Theorems" => Rewrite_Inst (subs, (xstr, ""))
1.200 | "Rulesets" => Rewrite_Set_Inst (subs, xstr)
1.201 - | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'")
1.202 + | str => error ("guh2rewtac: not impl. for '"^xstr^"'")
1.203 end;
1.204 (*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" [];
1.205 val it = Rewrite ("constant_mult_square", "") : tac