1.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml	Mon Dec 07 09:52:54 2015 +0100
     1.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml	Mon Dec 07 10:01:49 2015 +0100
     1.3 @@ -567,12 +567,12 @@
     1.4  fun thm''2xml j (thm : thm) =
     1.5      indt j ^ "<THEOREM>\n" ^
     1.6      indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
     1.7 -    term2xml j (prop_of thm) ^ "\n" ^
     1.8 +    term2xml j (Thm.prop_of thm) ^ "\n" ^
     1.9      indt j ^ "</THEOREM>\n" : xml;
    1.10  fun xml_of_thm (thm : thm) =
    1.11    XML.Elem (("THEOREM", []), [
    1.12      XML.Elem (("ID", []), [XML.Text (thmID_of_derivation_name' thm)]),
    1.13 -    xml_of_term (prop_of thm)])
    1.14 +    xml_of_term (Thm.prop_of thm)])
    1.15  
    1.16  fun scr2xml j EmptyScr =
    1.17      indt j ^"<SCRIPT>  </SCRIPT>\n" : xml