1.1 --- a/src/sml/IsacKnowledge/Integrate.ML Thu Feb 21 17:09:19 2008 +0100
1.2 +++ b/src/sml/IsacKnowledge/Integrate.ML Fri Feb 22 16:56:31 2008 +0100
1.3 @@ -41,11 +41,24 @@
1.4 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
1.5 end;
1.6
1.7 +(*WN080222
1.8 (*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*)
1.9 fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
1.10 Some ((term2str p) ^ " = " ^ term2str (new_c p),
1.11 Trueprop $ (mk_equality (p, new_c p)))
1.12 | eval_new_c _ _ _ _ = None;
1.13 +*)
1.14 +
1.15 +(*WN080222:*)
1.16 +(*("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "#add_new_c_"))
1.17 + this is _not in_ the term, because only applied to _whole_ term*)
1.18 +fun eval_add_new_c _ _ (p as (Const ("Integrate.add'_new'_c",_) $ t)) _ =
1.19 + Some ((term2str p) ^ " = " ^ term2str (new_c p),
1.20 + Trueprop $ (mk_equality (p, new_c p)))
1.21 + | eval_add_new_c _ _ (p as (Const ("Integrate.add'_new'_c",_) $ t)) _ =
1.22 + Some ((term2str p) ^ " = " ^ term2str (new_c p),
1.23 + Trueprop $ (mk_equality (p, new_c p)))
1.24 + | eval_add_new_c _ _ _ _ = None;
1.25
1.26 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
1.27 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
1.28 @@ -58,7 +71,8 @@
1.29 | eval_is_f_x _ _ _ _ = None;
1.30
1.31 calclist':= overwritel (!calclist',
1.32 - [("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),
1.33 + [(*("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),*)
1.34 + ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
1.35 ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))
1.36 ]);
1.37
1.38 @@ -107,8 +121,8 @@
1.39 ],
1.40 scr = EmptyScr},
1.41 srls = Erls, calc = [],
1.42 - rules = [ Thm ("call_for_new_c", num_str call_for_new_c),
1.43 - Calc("Integrate.new'_c", eval_new_c "new_c_")
1.44 + rules = [ (*Thm ("call_for_new_c", num_str call_for_new_c),*)
1.45 + Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.46 ],
1.47 scr = EmptyScr};
1.48
2.1 --- a/src/sml/IsacKnowledge/Integrate.thy Thu Feb 21 17:09:19 2008 +0100
2.2 +++ b/src/sml/IsacKnowledge/Integrate.thy Fri Feb 22 16:56:31 2008 +0100
2.3 @@ -16,7 +16,7 @@
2.4 consts
2.5
2.6 Integral :: "[real, real]=> real" ("Integral _ D _" 91)
2.7 - new'_c :: "real => real" ("new'_c _" 66)
2.8 +(*new'_c :: "real => real" ("new'_c _" 66)*)
2.9 is'_f'_x :: "real => bool" ("_ is'_f'_x" 10)
2.10
2.11 (*descriptions in the related problems*)
2.12 @@ -45,9 +45,10 @@
2.13 \(Integral u D bdv) + (Integral v D bdv)"
2.14 integral_mult "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> \
2.15 \Integral (u * v) D bdv = u * (Integral v D bdv)"
2.16 +(*WN080222: this goes into sub-terms, too ...
2.17 call_for_new_c "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> \
2.18 \a = a + new_c a"
2.19 -
2.20 +*)
2.21 integral_pow "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
2.22
2.23 end
2.24 \ No newline at end of file
3.1 --- a/src/sml/ME/rewtools.sml Thu Feb 21 17:09:19 2008 +0100
3.2 +++ b/src/sml/ME/rewtools.sml Fri Feb 22 16:56:31 2008 +0100
3.3 @@ -134,6 +134,29 @@
3.4 end)
3.5 handle _ => raise error "derive_norm, Calc: no rewrite"
3.6 end
3.7 +(* TODO.WN080222: see rewrite__set_
3.8 + @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
3.9 + | Cal1 (cc as (op_,_)) =>
3.10 + (let val _= if !trace_rewrite andalso i < ! depth then
3.11 + writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
3.12 + val ct = app_num_tr'2 ct
3.13 + in case get_calculation_ thy cc ct of
3.14 + None => (ct, asm)
3.15 + | Some (thmid, thm') =>
3.16 + let
3.17 + val pairopt =
3.18 + rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
3.19 + ((#erls o rep_rls) rls) put_asm thm' ct;
3.20 + val _ = if pairopt <> None then ()
3.21 + else raise error("rewrite_set_, rewrite_ \""^
3.22 + (string_of_thmI thm')^"\" "^(term2str ct)^" = None")
3.23 + val _ = if ! trace_rewrite andalso i < ! depth
3.24 + then writeln((idt"="(i+1))^" cal1. to: "^
3.25 + (term2str ((fst o the) pairopt)))
3.26 + else()
3.27 + in the pairopt end
3.28 + end)
3.29 +@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.30 | Rls_ rls =>
3.31 (case rewrite_set_ thy true rls t of
3.32 None => rew_once lim rts t apno rs'
3.33 @@ -602,6 +625,7 @@
3.34 fun thm_of_rule Erule = []
3.35 | thm_of_rule (thm as Thm _) = [thm]
3.36 | thm_of_rule (Calc _) = []
3.37 + | thm_of_rule (Cal1 _) = []
3.38 | thm_of_rule (Rls_ rls) = thms_of_rls rls
3.39 and thms_of_rls Erls = []
3.40 | thms_of_rls (Rls {rules,...}) = (flat o (map thm_of_rule)) rules
3.41 @@ -638,6 +662,10 @@
3.42 (case get_calculation_ thy c f of
3.43 Some (str, _) => [rule2tac [] cal]
3.44 | None => [])
3.45 + | try_rew thy _ _ _ f (cal as Cal1 c) =
3.46 + (case get_calculation_ thy c f of
3.47 + Some (str, _) => [rule2tac [] cal]
3.48 + | None => [])
3.49 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
3.50 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) =
3.51 distinct (flat (map (try_rew thy ro erls subst f) rules))
4.1 --- a/src/sml/Scripts/Script.thy Thu Feb 21 17:09:19 2008 +0100
4.2 +++ b/src/sml/Scripts/Script.thy Fri Feb 22 16:56:31 2008 +0100
4.3 @@ -37,6 +37,7 @@
4.4 ("(Rewrite'_Set'_Inst (_ _ _))" 11)
4.5 (*without last argument ^^ for @@*)
4.6 Calculate :: "[ID, 'a] => 'a"
4.7 + Calculate1 :: "[ID, 'a] => 'a" (*FIXXXME: unknown to script-interpreter*)
4.8
4.9 (* WN0509 substitution now is rewriting by a list of terms (of type bool)
4.10 Substitute :: "[(real * real) list, 'a] => 'a"*)
5.1 --- a/src/sml/Scripts/rewrite.sml Thu Feb 21 17:09:19 2008 +0100
5.2 +++ b/src/sml/Scripts/rewrite.sml Fri Feb 22 16:56:31 2008 +0100
5.3 @@ -130,7 +130,7 @@
5.4 fun rew_once ruls asm ct Noap [] = (ct,asm)
5.5 | rew_once ruls asm ct Appl [] =
5.6 (case rls of Rls _ => rew_once ruls asm ct Noap ruls
5.7 - | Seq _ => (ct,asm))
5.8 + | Seq _ => (ct,asm))
5.9 | rew_once ruls asm ct apno (rul::thms) =
5.10 (* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls);
5.11 val Thm (thmid, thm) = rul;
5.12 @@ -167,6 +167,29 @@
5.13 else()
5.14 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end
5.15 end)
5.16 +(* use"Scripts/rewrite.sml";
5.17 + @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
5.18 + | Cal1 (cc as (op_,_)) =>
5.19 + (let val _= if !trace_rewrite andalso i < ! depth then
5.20 + writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
5.21 + val ct = app_num_tr'2 ct
5.22 + in case get_calculation_ thy cc ct of
5.23 + None => (ct, asm)
5.24 + | Some (thmid, thm') =>
5.25 + let
5.26 + val pairopt =
5.27 + rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
5.28 + ((#erls o rep_rls) rls) put_asm thm' ct;
5.29 + val _ = if pairopt <> None then ()
5.30 + else raise error("rewrite_set_, rewrite_ \""^
5.31 + (string_of_thmI thm')^"\" "^(term2str ct)^" = None")
5.32 + val _ = if ! trace_rewrite andalso i < ! depth
5.33 + then writeln((idt"="(i+1))^" cal1. to: "^
5.34 + (term2str ((fst o the) pairopt)))
5.35 + else()
5.36 + in the pairopt end
5.37 + end)
5.38 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
5.39 | Rls_ rls' =>
5.40 (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
5.41 Some (t',asm') => rew_once ruls (asm union asm') t' Appl thms
6.1 --- a/src/sml/Scripts/scrtools.sml Thu Feb 21 17:09:19 2008 +0100
6.2 +++ b/src/sml/Scripts/scrtools.sml Fri Feb 22 16:56:31 2008 +0100
6.3 @@ -345,6 +345,9 @@
6.4 val Cal $ _ =
6.5 ((inst_abs thy) o term_of o the o (parseN thy))
6.6 "Calculate plus";
6.7 +val Ca1 $ _ =
6.8 + ((inst_abs thy) o term_of o the o (parseN thy))
6.9 + "Calculate1 plus";
6.10 val Rew $ (Free (_,IDtype)) $ _ $ t_ =
6.11 ((inst_abs thy) o term_of o the o (parseN thy))
6.12 "Rewrite real_diff_minus False t_";
6.13 @@ -367,6 +370,8 @@
6.14 Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const))
6.15 | rule2stac calc (Calc (c, _)) =
6.16 Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
6.17 + | rule2stac calc (Cal1 (c, _)) =
6.18 + Try $ (Repeat $ (Ca1 $ Free (assoc_calc (calc ,c), IDtype)))
6.19 | rule2stac _ (Rls_ rls) =
6.20 Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);
6.21 (*val t = rule2stac [] (Thm ("real_diff_minus", num_str real_diff_minus));
6.22 @@ -381,6 +386,8 @@
6.23 HOLogic.false_const))
6.24 | rule2stac_inst calc (Calc (c, _)) =
6.25 Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
6.26 + | rule2stac_inst calc (Cal1 (c, _)) =
6.27 + Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
6.28 | rule2stac_inst _ (Rls_ rls) =
6.29 Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $
6.30 HOLogic.false_const);
6.31 @@ -416,6 +423,7 @@
6.32 then contain_bdv rs
6.33 else true
6.34 | contain_bdv (Calc _ ::rs) = contain_bdv rs
6.35 + | contain_bdv (Cal1 _ ::rs) = contain_bdv rs
6.36 | contain_bdv (Rls_ rls ::rs) =
6.37 contain_bdv (get_rules rls) orelse contain_bdv rs
6.38 | contain_bdv (r::_) =
6.39 @@ -428,6 +436,8 @@
6.40 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ t_))
6.41 else ScrStep $ Term $
6.42 (Repeat $ (((@@ o (map (rule2stac calc))) rules) $ t_));
6.43 +(* val (calc, rules) = (!calclist', rules);
6.44 + *)
6.45 fun rules2scr_Seq calc rules =
6.46 if contain_bdv rules
6.47 then ScrStep_inst $ Term $ Bdv $
6.48 @@ -449,6 +459,8 @@
6.49 (filter is_calc) o stacpbls) sc,
6.50 rules=rules,
6.51 scr = Script sc} end
6.52 +(* val (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) = add_new_c;
6.53 + *)
6.54 | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) =
6.55 let val sc = (rules2scr_Seq (!calclist') rules)
6.56 in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
7.1 --- a/src/sml/calcelems.sml Thu Feb 21 17:09:19 2008 +0100
7.2 +++ b/src/sml/calcelems.sml Fri Feb 22 16:56:31 2008 +0100
7.3 @@ -58,11 +58,14 @@
7.4
7.5
7.6 datatype rule =
7.7 - Erule (*WN.3.6.03 for rep_tac_ Check_elementwise*)
7.8 -| Thm of (string * thm)
7.9 -| Calc of string * (*check for equality*)
7.10 + Erule (*.the empty rule .*)
7.11 +| Thm of (string * thm)(*.a theorem, ie (identifier, Thm.thm).*)
7.12 +| Calc of string * (*.sml-code manipulating a (sub)term .*)
7.13 (string -> term -> theory -> (string * term) option)
7.14 -| Rls_ of rls (*.ie. rule sets may be nested.*)
7.15 +| Cal1 of string * (*.sml-code applied only to whole term
7.16 + or left/right-hand-side of eqality .*)
7.17 + (string -> term -> theory -> (string * term) option)
7.18 +| Rls_ of rls (*.ie. rule sets may be nested.*)
7.19 and scr =
7.20 EmptyScr
7.21 | Script of term (*for met*)
7.22 @@ -166,15 +169,18 @@
7.23 fun rule2str Erule = "Erule"
7.24 | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
7.25 | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
7.26 + | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
7.27 | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
7.28 fun rule2str' Erule = "Erule"
7.29 | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
7.30 | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
7.31 + | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
7.32 | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
7.33
7.34 (*WN080102 compare eq_rule ?!?*)
7.35 fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
7.36 | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
7.37 + | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
7.38 | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
7.39 | eqrule _ = false;
7.40
8.1 --- a/src/sml/xmlsrc/datatypes.sml Thu Feb 21 17:09:19 2008 +0100
8.2 +++ b/src/sml/xmlsrc/datatypes.sml Fri Feb 22 16:56:31 2008 +0100
8.3 @@ -193,6 +193,7 @@
8.4 termop ^ " </GUH>\n" ^
8.5 indt j ^ "</RULE>\n"
8.6 *)
8.7 + | rule2xml j thyID (Cal1 (termop, _)) = ""
8.8 | rule2xml j thyID (Rls_ rls) =
8.9 let val rls' = (#id o rep_rls) rls
8.10 in indt j ^ "<RULE>\n" ^
8.11 @@ -429,6 +430,10 @@
8.12 fun prepat2xml j [] = ""
8.13 | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
8.14
8.15 +(* val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
8.16 + srls, calc, rules, scr})) =
8.17 + (j, (thyID, "Seq", data));
8.18 + *)
8.19 fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
8.20 srls, calc, rules, scr}) =
8.21 indt j ^"<RULESET>\n"^
8.22 @@ -468,8 +473,11 @@
8.23 erls=erls,srls=srls,calc=calc,rules=rules,scr=scr});
8.24 val (j, (thyID, Rls {id, preconds, rew_ord=(ord,_), erls,
8.25 srls, calc, rules, scr})) = (i, thy_rls);
8.26 + val (j, (thyID, Seq data)) = (i, thy_rls);
8.27 *)
8.28 | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
8.29 +(* val (j, (thyID, Seq data)) = (i, thy_rls);
8.30 + *)
8.31 | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
8.32 | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, scr}) =
8.33 indt j ^"<RULESET>\n"^
9.1 --- a/src/sml/xmlsrc/thy-hierarchy.sml Thu Feb 21 17:09:19 2008 +0100
9.2 +++ b/src/sml/xmlsrc/thy-hierarchy.sml Fri Feb 22 16:56:31 2008 +0100
9.3 @@ -211,7 +211,7 @@
9.4 (**.create the xml-files for the theory-data from the hierarchy.**)
9.5
9.6 val i = indentation;
9.7 -(*analoguous to 'fun met2xml'*)
9.8 +(*.analoguous to 'fun met2xml'.*)
9.9 fun thydata2xml (theID:theID, Html {guh, coursedesign, mathauthors, html}) =
9.10 "<HTMLDATA>\n" ^
9.11 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
9.12 @@ -236,7 +236,7 @@
9.13 authors2xml i "COURSEDESIGNS" coursedesign ^
9.14 "</THEOREMDATA>\n"
9.15 (* val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
9.16 - (theID, rlsdata);
9.17 + (theID, thydata);
9.18 *)
9.19 | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
9.20 "<RULESETDATA>\n" ^
10.1 --- a/src/smltest/xmlsrc/thy-hierarchy.sml Thu Feb 21 17:09:19 2008 +0100
10.2 +++ b/src/smltest/xmlsrc/thy-hierarchy.sml Fri Feb 22 16:56:31 2008 +0100
10.3 @@ -18,6 +18,7 @@
10.4 "----------- fun thydata2xml -------------------------------------";
10.5 "----------- write xml to tmp ------------------------------------";
10.6 "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
10.7 +"----------- ### thes2file ... Exception- Match raised -----------";
10.8 "-----------------------------------------------------------------";
10.9 "-----------------------------------------------------------------";
10.10 "-----------------------------------------------------------------";
10.11 @@ -52,16 +53,16 @@
10.12 "collect_thms thy'------------------------------------------------";
10.13 (thms_of thy);
10.14
10.15 -(apfst single) ("Integrate.call_for_new_c", call_for_new_c);
10.16 +(apfst single) ("Integrate.integral_var", integral_var);
10.17
10.18 -(strip_thy o #1) ("Integrate.call_for_new_c", call_for_new_c);
10.19 +(strip_thy o #1) ("Integrate.integral_var", integral_var);
10.20
10.21 (*cannot get this as arg from arg ^^^^^^^^^^^^^^^^*)
10.22 - ("Integrate.call_for_new_c", call_for_new_c);
10.23 + ("Integrate.integral_var", integral_var);
10.24 (*thus new fun....*)
10.25
10.26 -makeHthm ("IsacKnowledge",thy') ("Integrate.call_for_new_c", call_for_new_c);
10.27 -(makeHthm ("IsacKnowledge",thy')) ("Integrate.call_for_new_c", call_for_new_c);
10.28 +makeHthm ("IsacKnowledge",thy') ("Integrate.integral_var", integral_var);
10.29 +(makeHthm ("IsacKnowledge",thy')) ("Integrate.integral_var", integral_var);
10.30 map (makeHthm ("IsacKnowledge",thy')) (thms_of thy);
10.31 collect_thms' ("IsacKnowledge",thy');
10.32
10.33 @@ -234,3 +235,32 @@
10.34 val it = () : unit
10.35 *** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]
10.36 *** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]*)
10.37 +
10.38 +"----------- ### thes2file ... Exception- Match raised -----------";
10.39 +"----------- ### thes2file ... Exception- Match raised -----------";
10.40 +"----------- ### thes2file ... Exception- Match raised -----------";
10.41 +writeln "what to do when you get,e.g. \n\
10.42 +\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\
10.43 +\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\
10.44 +\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\
10.45 +\Exception- Match raised";
10.46 +
10.47 +val ptyp = hd (!thehier);
10.48 +val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];
10.49 +val thydata = get_the theID;
10.50 +(* creates a file ...
10.51 +thydata2file "~/tmp/"[] theID thydata (*reports Exception- Match in question*);
10.52 +*)
10.53 +thydata2xml (theID, thydata) (*reports Exception- Match in question*);
10.54 +val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
10.55 + (theID, thydata);
10.56 +rls2xml i thy_rls (*reports Exception- Match in question*);
10.57 +val (j, (thyID, Seq data)) = (i, thy_rls);
10.58 +(* evaluate this local fun ...
10.59 +rls2xm j (thyID, "Seq", data) (*reports Exception- Match in question*);
10.60 +*)
10.61 +val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
10.62 + srls, calc, rules, scr})) =
10.63 + (j, (thyID, "Seq", data));
10.64 +rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);
10.65 +