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 ===========================