1.1 --- a/src/Tools/isac/calcelems.sml	Thu May 24 17:13:58 2012 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu May 24 18:40:07 2012 +0200
     1.3 @@ -18,7 +18,10 @@
     1.4  val empty_cterm' = "empty_cterm'";
     1.5  
     1.6  type thmID = string;    (* identifier for a thm (the shortest possible identifier)       *)
     1.7 -type thmDeriv = string; (* thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name *)
     1.8 +type thmDeriv = string; (* WN120524 deprecated
     1.9 +  thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name 
    1.10 +  WN120524: dont use Thm.derivation_name, this is destroyed by num_str;
    1.11 +  Thm.get_name_hint survives num_str and seems perfectly reliable *)
    1.12  
    1.13  type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
    1.14  type thm'' = thmID * term;
    1.15 @@ -151,6 +154,9 @@
    1.16  
    1.17  fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
    1.18  fun thyID_of_derivation_name dn = hd (space_explode "." dn);
    1.19 +fun thm'_of_thm thm =
    1.20 +  ((thyID_of_derivation_name o Thm.get_name_hint) thm,
    1.21 +   (thmID_of_derivation_name o Thm.get_name_hint) thm): thm'
    1.22  
    1.23  fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
    1.24      (strip_thy thmid1) = (strip_thy thmid2);