1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Mon Dec 07 09:52:54 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Mon Dec 07 10:01:49 2015 +0100
     1.3 @@ -236,11 +236,11 @@
     1.4  
     1.5  (**.set up isab_thm_thy in Isac.ML.**)
     1.6  
     1.7 -fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, prop_of thm));
     1.8 +fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, Thm.prop_of thm));
     1.9  (* WN120320: reconsider design since thmID and thyID can be retrieved from thm: *)
    1.10  fun rearrange' (thmID, thm) =
    1.11    (thmID_of_derivation_name thmID,
    1.12 -    (thyID_of_derivation_name thmID, prop_of thm)): (thmID * (thyID * term));
    1.13 +    (thyID_of_derivation_name thmID, Thm.prop_of thm)): (thmID * (thyID * term));
    1.14  fun rearrange_inv (thmID, (thyID, term)) = (thyID, (thmID, term));
    1.15  
    1.16  (*================= version before Isbelle2002 --> 2011 ===========================

     2.1 --- a/src/Tools/isac/calcelems.sml	Mon Dec 07 09:52:54 2015 +0100
     2.2 +++ b/src/Tools/isac/calcelems.sml	Mon Dec 07 10:01:49 2015 +0100
     2.3 @@ -297,8 +297,8 @@
     2.4  
     2.5  
     2.6  (*check for [.] as caused by "fun assoc_thm'"*)
     2.7 -fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (prop_of thm)
     2.8 -fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (prop_of thm)
     2.9 +fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (Thm.prop_of thm)
    2.10 +fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (Thm.prop_of thm)
    2.11  fun string_of_thmI thm =
    2.12    let 
    2.13      val str = (de_quote o string_of_thm) thm

     3.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml	Mon Dec 07 09:52:54 2015 +0100
     3.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml	Mon Dec 07 10:01:49 2015 +0100
     3.3 @@ -567,12 +567,12 @@
     3.4  fun thm''2xml j (thm : thm) =
     3.5      indt j ^ "<THEOREM>\n" ^
     3.6      indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
     3.7 -    term2xml j (prop_of thm) ^ "\n" ^
     3.8 +    term2xml j (Thm.prop_of thm) ^ "\n" ^
     3.9      indt j ^ "</THEOREM>\n" : xml;
    3.10  fun xml_of_thm (thm : thm) =
    3.11    XML.Elem (("THEOREM", []), [
    3.12      XML.Elem (("ID", []), [XML.Text (thmID_of_derivation_name' thm)]),
    3.13 -    xml_of_term (prop_of thm)])
    3.14 +    xml_of_term (Thm.prop_of thm)])
    3.15  
    3.16  fun scr2xml j EmptyScr =
    3.17      indt j ^"<SCRIPT>  </SCRIPT>\n" : xml