1.1 --- a/src/Tools/isac/calcelems.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -144,9 +144,9 @@
1.4 val e_rule =
1.5 Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" );
1.6 fun id_of_thm (Thm (id, _)) = id
1.7 - | id_of_thm _ = raise error "id_of_thm";
1.8 + | id_of_thm _ = error "id_of_thm";
1.9 fun thm_of_thm (Thm (_, thm)) = thm
1.10 - | thm_of_thm _ = raise error "thm_of_thm";
1.11 + | thm_of_thm _ = error "thm_of_thm";
1.12 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
1.13 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
1.14 (strip_thy thmid1) = (strip_thy thmid2);
1.15 @@ -307,7 +307,7 @@
1.16 (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
1.17 fun theID2thyID (theID:theID) =
1.18 if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
1.19 - else raise error ("theID2thyID called with "^ theID2str theID);
1.20 + else error ("theID2thyID called with "^ theID2str theID);
1.21
1.22 (*the key into the hierarchy ob problems*)
1.23 type pblID = string list; (* domID::...*)
1.24 @@ -451,9 +451,9 @@
1.25 (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.26 | rep_rls Erls = rep_rls e_rls
1.27 | rep_rls (Rrls {id,...}) = rep_rls e_rls
1.28 - (*raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
1.29 + (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
1.30 (*| rep_rls (Seq {id,...}) =
1.31 - raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
1.32 + error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
1.33 --1.7.03*)
1.34 fun rep_rrls
1.35 (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
1.36 @@ -464,9 +464,9 @@
1.37 rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
1.38 locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
1.39 | rep_rrls (Rls {id,...}) =
1.40 - raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
1.41 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
1.42 | rep_rrls (Seq {id,...}) =
1.43 - raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
1.44 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
1.45
1.46 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.47 rules =rs,scr=sc}) r =
1.48 @@ -477,7 +477,7 @@
1.49 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.50 rules = rs @ r,scr=sc}:rls)
1.51 | append_rls id (Rrls _) _ =
1.52 - raise error ("append_rls: not for reverse-rewrite-rule-set "^id);
1.53 + error ("append_rls: not for reverse-rewrite-rule-set "^id);
1.54
1.55 (*. are _atomic_ rules equal ?.*)
1.56 (*WN080102 compare eqrule ?!?*)
1.57 @@ -516,7 +516,7 @@
1.58 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.59 scr=sc1}:rls)
1.60 | merge_rls _ _ _ =
1.61 - raise error "merge_rls: not for reverse-rewrite-rule-sets\
1.62 + error "merge_rls: not for reverse-rewrite-rule-sets\
1.63 \and not for mixed Rls -- Seq";
1.64 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.65 (*asm_thm=at,*)rules =rs,scr=sc}) r =
1.66 @@ -528,7 +528,7 @@
1.67 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.68 (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.69 scr=sc}:rls)
1.70 - | remove_rls id (Rrls _) _ = raise error
1.71 + | remove_rls id (Rrls _) _ = error
1.72 ("remove_rls: not for reverse-rewrite-rule-set "^id);
1.73
1.74 (*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
1.75 @@ -540,29 +540,29 @@
1.76 SOME _ => true | NONE => false;*)
1.77 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
1.78 | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
1.79 - | memrls r _ = raise error ("memrls: incomplete impl. r= "^(rule2str r));
1.80 + | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
1.81 fun rls_get_thm rls (id: xstring) =
1.82 case find_first (curry eq_rule e_rule)
1.83 ((#rules o rep_rls) rls) of
1.84 SOME thm => SOME thm | NONE => NONE;
1.85
1.86 -fun assoc' ([], key) = raise error ("ME_Isa: '"^key^"' not known")
1.87 +fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
1.88 | assoc' ((keyi, xi) :: pairs, key) =
1.89 if key = keyi then SOME xi else assoc' (pairs, key);
1.90
1.91 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
1.92 - handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");*)
1.93 + handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
1.94 fun assoc_thy (thy:theory') = (*FIXME100818 abolish*)
1.95 (theory ((implode o (curry takelast 4) o explode) thy))
1.96 - handle _ => raise error ("ME_Isa: thy '" ^ thy ^ "' not in system");
1.97 + handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
1.98
1.99 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
1.100 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
1.101 overlays by re-using an identifier in different thys.*)
1.102 fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
1.103 - handle _ => raise error ("ME_Isa: '"^rls^"' not in system");
1.104 + handle _ => error ("ME_Isa: '"^rls^"' not in system");
1.105 (*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
1.106 - handle _ => raise error ("ME_Isa: '"^rls^"' not in system");*)
1.107 + handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
1.108
1.109 (*.overwrite an element in an association list and pair it with a thyID
1.110 in order to create the thy_hierarchy;
1.111 @@ -579,20 +579,20 @@
1.112 in overwritel (al, bl') end;
1.113
1.114 fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
1.115 - handle _ => raise error ("ME_Isa: rew_ord '"^ro^"' not in system");
1.116 + handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
1.117 (*get the string for stac from rule*)
1.118 -fun assoc_calc ([], key) = raise error ("assoc_calc: '"^ key ^"' not found")
1.119 +fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found")
1.120 | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
1.121 if key = keyi then calc else assoc_calc (pairs, key);
1.122 (*only used for !calclist'...*)
1.123 -fun assoc1 ([], key) = raise error ("assoc1 (for met.calc=): '"^ key
1.124 +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
1.125 ^"' not found")
1.126 | assoc1 ((all as (keyi, _)) :: pairs, key) =
1.127 if key = keyi then all else assoc1 (pairs, key);
1.128
1.129 (*TODO.WN080102 clarify usage of type cal and type calc..*)
1.130 fun calID2calcID (calID : calID) =
1.131 - let fun ass [] = raise error ("calID2calcID: "^calID^"not in calclist'")
1.132 + let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
1.133 | ass ((calci, (cali, eval_fn))::ids) =
1.134 if calID = cali then calci
1.135 else ass ids