1.1 --- a/src/Tools/isac/calcelems.sml	Thu Oct 06 17:03:44 2016 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Mon Oct 10 18:24:14 2016 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  thmID            : type for data from user input + program
     1.5  thmDeriv         : type for thy_hierarchy ONLY
     1.6  obsolete types   : thm' (SEE "ad thm'"), thm''. 
     1.7 -revise funs      : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm'_of_thm thm.
     1.8 +revise funs      : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
     1.9  activate         : thmID_of_derivation_name'
    1.10  *)
    1.11  type iterID = int;
    1.12 @@ -37,7 +37,7 @@
    1.13    Thm.get_name_hint survives num_str and seems perfectly reliable *)
    1.14  
    1.15  type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
    1.16 -type thm'' = thmID * term;
    1.17 +type thm'' = thmID * term; (* only for transport via libisabelle isac-java <--- ME *)
    1.18  type rls' = string;
    1.19  
    1.20  (*.a 'guh'='globally unique handle' is a string unique for each element
    1.21 @@ -286,6 +286,7 @@
    1.22  fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
    1.23  fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
    1.24  fun thyID_of_derivation_name dn = hd (space_explode "." dn);
    1.25 +fun thm''_of_thm thm = (thmID_of_derivation_name' thm, Thm.prop_of thm) : thm''
    1.26  
    1.27  fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
    1.28      (strip_thy thmid1) = (strip_thy thmid2);
    1.29 @@ -309,9 +310,6 @@
    1.30      | _ => str
    1.31    end
    1.32  
    1.33 -fun thm'_of_thm thm =
    1.34 -  ((thmID_of_derivation_name o Thm.get_name_hint) thm, string_of_thmI thm): thm'
    1.35 -
    1.36  (*.id requested for all, Rls,Seq,Rrls.*)
    1.37  fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
    1.38    | id_rls (Rls {id,...}) = id