1.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml	Sat Aug 15 08:06:28 2015 +0200
     1.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml	Sat Aug 15 08:55:27 2015 +0200
     1.3 @@ -788,20 +788,20 @@
     1.4    | xml_of_tac (Rewrite_Set rls') =
     1.5      XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
     1.6    | xml_of_tac (Rewrite_Set_Inst (subs, rls')) =
     1.7 -    XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), (
     1.8 -      XML.Elem (("RULESET", []), [XML.Text rls']) ::
     1.9 -      xml_of_subs subs ::[]))
    1.10 -    (*----- TERMTACTIC ---------------------------------------------------*)
    1.11 +    XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([
    1.12 +      xml_of_subs subs,
    1.13 +      XML.Elem (("RULESET", []), [XML.Text rls'])]))
    1.14 +    (*----- FORMTACTIC ---------------------------------------------------*)
    1.15    | xml_of_tac (Add_Find ct) =
    1.16 -    XML.Elem (("TERMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
    1.17 +    XML.Elem (("FORMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
    1.18    | xml_of_tac (Add_Given ct) =
    1.19 -    XML.Elem (("TERMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
    1.20 +    XML.Elem (("FORMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
    1.21    | xml_of_tac (Add_Relation ct) =
    1.22 -    XML.Elem (("TERMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
    1.23 +    XML.Elem (("FORMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
    1.24    | xml_of_tac (Check_elementwise ct) =
    1.25 -    XML.Elem (("TERMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
    1.26 +    XML.Elem (("FORMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
    1.27    | xml_of_tac (Take ct) =
    1.28 -    XML.Elem (("TERMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
    1.29 +    XML.Elem (("FORMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
    1.30      (*----- SIMPLETACTIC -------------------------------------------------*)
    1.31    | xml_of_tac (Calculate opstr) =
    1.32      XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
    1.33 @@ -845,23 +845,23 @@
    1.34    | xml_to_tac
    1.35      (XML.Elem (("REWRITESETINSTTACTIC", [
    1.36        ("name", "Rewrite_Set_Inst")]), [
    1.37 -        XML.Elem (("RULESET", []), [XML.Text rls']),
    1.38 -        subs])) = Rewrite_Set_Inst (xml_to_subs subs, rls')
    1.39 -    (*----- TERMTACTIC ---------------------------------------------------*)
    1.40 +        subs,
    1.41 +        XML.Elem (("RULESET", []), [XML.Text rls'])])) = Rewrite_Set_Inst (xml_to_subs subs, rls')
    1.42 +    (*----- FORMTACTIC ---------------------------------------------------*)
    1.43    | xml_to_tac
    1.44 -    (XML.Elem (("TERMTACTIC", [
    1.45 +    (XML.Elem (("FORMTACTIC", [
    1.46        ("name", "Add_Find")]), [ct])) =  Add_Find (xml_to_cterm ct)
    1.47    | xml_to_tac
    1.48 -    (XML.Elem (("TERMTACTIC", [
    1.49 +    (XML.Elem (("FORMTACTIC", [
    1.50        ("name", "Add_Given")]), [ct])) = Add_Given (xml_to_cterm ct)
    1.51    | xml_to_tac
    1.52 -    (XML.Elem (("TERMTACTIC", [
    1.53 +    (XML.Elem (("FORMTACTIC", [
    1.54        ("name", "Add_Relation")]), [ct])) = Add_Relation (xml_to_cterm ct)
    1.55    | xml_to_tac
    1.56 -    (XML.Elem (("TERMTACTIC", [
    1.57 +    (XML.Elem (("FORMTACTIC", [
    1.58        ("name", "Take")]), [ct])) = Take (xml_to_cterm ct)
    1.59    | xml_to_tac
    1.60 -    (XML.Elem (("TERMTACTIC", [
    1.61 +    (XML.Elem (("FORMTACTIC", [
    1.62        ("name", "Check_elementwise")]), [ct])) = Check_elementwise (xml_to_cterm ct)
    1.63      (*----- SIMPLETACTIC -------------------------------------------------*)
    1.64    | xml_to_tac

     2.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml	Sat Aug 15 08:06:28 2015 +0200
     2.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml	Sat Aug 15 08:55:27 2015 +0200
     2.3 @@ -177,7 +177,7 @@
     2.4      </PAIR>
     2.5    </SUBSTITUTION>
     2.6  </REWRITESETINSTTACTIC>:*)
     2.7 -if xmlstr 0 (xml_of_tac tac) = "<REWRITESETINSTTACTIC name=Rewrite_Set_Inst>\n. <RULESET>\n. . simplify\n. </RULESET>\n. <SUBSTITUTION>\n. . <PAIR>\n. . . <VARIABLE>\n. . . . <MATHML>\n. . . . . <ISA>\n. . . . . . bdv\n. . . . . </ISA>\n. . . . </MATHML>\n. . . </VARIABLE>\n. . . <VALUE>\n. . . . <MATHML>\n. . . . . <ISA>\n. . . . . . x\n. . . . . </ISA>\n. . . . </MATHML>\n. . . </VALUE>\n. . </PAIR>\n. </SUBSTITUTION>\n</REWRITESETINSTTACTIC>\n"
     2.8 +if xmlstr 0 (xml_of_tac tac) = "<REWRITESETINSTTACTIC name=Rewrite_Set_Inst>\n. <SUBSTITUTION>\n. . <PAIR>\n. . . <VARIABLE>\n. . . . <MATHML>\n. . . . . <ISA>\n. . . . . . bdv\n. . . . . </ISA>\n. . . . </MATHML>\n. . . </VARIABLE>\n. . . <VALUE>\n. . . . <MATHML>\n. . . . . <ISA>\n. . . . . . x\n. . . . . </ISA>\n. . . . </MATHML>\n. . . </VALUE>\n. . </PAIR>\n. </SUBSTITUTION>\n. <RULESET>\n. . simplify\n. </RULESET>\n</REWRITESETINSTTACTIC>\n"
     2.9  then () else error "xml_of_tac Rewrite_Set_Inst CHANGED";
    2.10  
    2.11  "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
    2.12 @@ -199,7 +199,7 @@
    2.13      <ISA>equality (x + 1 = 2)</ISA>
    2.14    </MATHML>
    2.15  </SIMPLETACTIC>*)
    2.16 -if xmlstr 0 (xml_of_tac tac) = "<TERMTACTIC name=Add_Given>\n. <MATHML>\n. . <ISA>\n. . . equality (x + 1 = 2)\n. . </ISA>\n. </MATHML>\n</TERMTACTIC>\n"
    2.17 +if xmlstr 0 (xml_of_tac tac) = "<FORMTACTIC name=Add_Given>\n. <MATHML>\n. . <ISA>\n. . . equality (x + 1 = 2)\n. . </ISA>\n. </MATHML>\n</FORMTACTIC>\n"
    2.18  then () else error "xml_of_tac Add_Given CHANGED";
    2.19  
    2.20  "----------- these are : string -> tac: ";