1.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml	Sat Aug 15 08:55:27 2015 +0200
     1.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml	Sat Aug 15 16:03:53 2015 +0200
     1.3 @@ -778,6 +778,9 @@
     1.4      XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
     1.5        XML.Elem (("THEORY", []), [XML.Text dI]),
     1.6        XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
     1.7 +  | xml_of_tac (Substitute cterms) =
     1.8 +    (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
     1.9 +    XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
    1.10      (*----- Rewrite* -----------------------------------------------------*)
    1.11    | xml_of_tac (Rewrite thm') =
    1.12      XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm' thm'])
    1.13 @@ -822,15 +825,16 @@
    1.14      XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
    1.15    | xml_of_tac (Specify_Problem ct) =
    1.16      XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
    1.17 -  | xml_of_tac (Substitute cterms) =
    1.18 -    (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
    1.19 -    XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
    1.20    | xml_of_tac tac = error ("xml_of_tac: not impl. for " ^ tac2str tac);
    1.21  
    1.22  fun xml_to_tac 
    1.23      (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
    1.24        XML.Elem (("THEORY", []), [XML.Text dI]),
    1.25        XML.Elem (("PROBLEM", []), [pI])])) = Subproblem (dI, xml_to_strs pI)
    1.26 +  | xml_to_tac
    1.27 +    (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
    1.28 +    (XML.Elem (("STRINGLISTTACTIC", [
    1.29 +      ("name", "Substitute")]), [cterms])) = Substitute (xml_to_sube cterms)
    1.30      (*----- Rewrite* -----------------------------------------------------*)
    1.31    | xml_to_tac
    1.32      (XML.Elem (("REWRITETACTIC", [
    1.33 @@ -891,10 +895,6 @@
    1.34    | xml_to_tac
    1.35      (XML.Elem (("STRINGLISTTACTIC", [
    1.36        ("name", "Specify_Problem")]), [ct])) = Specify_Problem (xml_to_strs ct)
    1.37 -  | xml_to_tac
    1.38 -    (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
    1.39 -    (XML.Elem (("STRINGLISTTACTIC", [
    1.40 -      ("name", "Substitute")]), [cterms])) = Substitute (xml_to_sube cterms)
    1.41    | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
    1.42  
    1.43  fun tacs2xml j [] = "":xml

     2.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml	Sat Aug 15 08:55:27 2015 +0200
     2.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml	Sat Aug 15 16:03:53 2015 +0200
     2.3 @@ -194,11 +194,11 @@
     2.4  Add_Given: cterm' -> tac;
     2.5  val tac = Add_Given("equality (x + 1 = 2)");
     2.6  xml_of_tac tac;(*
     2.7 -<SIMPLETACTIC name="Add_Given">
     2.8 +<FORMTACTIC name="Add_Given">
     2.9    <MATHML>
    2.10      <ISA>equality (x + 1 = 2)</ISA>
    2.11    </MATHML>
    2.12 -</SIMPLETACTIC>*)
    2.13 +</FORMTACTIC>*)
    2.14  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.15  then () else error "xml_of_tac Add_Given CHANGED";
    2.16