1.1 --- a/src/Tools/isac/calcelems.sml	Thu Jul 24 17:22:21 2014 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sat Jul 26 13:39:00 2014 +0200
     1.3 @@ -17,6 +17,15 @@
     1.4  type cterm' = string;
     1.5  val empty_cterm' = "empty_cterm'";
     1.6  
     1.7 +(* TODO CLEANUP Thm:
     1.8 +type rule = Thm : (a) needs no identifier since reflection is built-in since Isabelle2011
     1.9 +                  (b) investigate if ""RS sym" attaches a [.]" still occurs: string_of_thmI
    1.10 +thmID           : user input + program
    1.11 +thmDeriv        : for thy_hierarchy ONLY
    1.12 +obsolete types  : thm' (SEE "ad thm'"), thm''. 
    1.13 +revise funs     : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm'_of_thm thm.
    1.14 +activate        : thmID_of_derivation_name'
    1.15 +*)
    1.16  type thmID = string;    (* identifier for a thm (the shortest possible identifier)       *)
    1.17  type thmDeriv = string; (* WN120524 deprecated
    1.18    thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name 
    1.19 @@ -103,7 +112,7 @@
    1.20  
    1.21  datatype rule =
    1.22    Erule                (*.the empty rule                     .*)
    1.23 -| Thm of (string * Basic_Thm.thm)(*.a theorem, ie (identifier, Thm.thm).*)
    1.24 +| Thm of (string * Basic_Thm.thm) (* see TODO CLEANUP Thm     *)
    1.25  | Calc of string *     (*.sml-code manipulating a (sub)term  .*)
    1.26  	  (string -> term -> theory -> (string * term) option)
    1.27  | Cal1 of string *     (*.sml-code applied only to whole term
    1.28 @@ -208,7 +217,7 @@
    1.29     (1) known by isabelle
    1.30     (2) not known, eg. calc_thm, instantiated rls
    1.31         the latter have a thmid "#..."
    1.32 -   and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
    1.33 +   and thus outside isa we ALWAYS transport both (thmID, string_of_thmI)
    1.34     and have a special assoc_thm / assoc_rls in this interface      *)
    1.35  type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
    1.36  type domID = string;   (* domID ^".thy" = theory' WN.101011 replace by thyID*)
    1.37 @@ -268,6 +277,7 @@
    1.38  fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
    1.39  
    1.40  fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
    1.41 +fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
    1.42  fun thyID_of_derivation_name dn = hd (space_explode "." dn);
    1.43  
    1.44  fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
    1.45 @@ -278,8 +288,6 @@
    1.46  fun eq_thmI' ((thmid1, _), (thmid2, _)) =
    1.47      (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
    1.48  
    1.49 -fun thm'_of_thm thm =
    1.50 -  ((thmID_of_derivation_name o Thm.get_name_hint) thm, ""): thm'
    1.51  
    1.52  (*check for [.] as caused by "fun assoc_thm'"*)
    1.53  fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (prop_of thm)
    1.54 @@ -292,15 +300,9 @@
    1.55        [" ", " ","[", ".", "]"] => implode a
    1.56      | _ => str
    1.57    end
    1.58 -(*
    1.59 -fun string_of_thmI thm =
    1.60 -    let val ct' = (de_quote o Thm.get_name_hint) thm
    1.61 -	val (a, b) = split_nlast (5, Symbol.explode ct')
    1.62 -    in case b of
    1.63 -	   [" ", " ","[", ".", "]"] => implode a
    1.64 -	 | _ => ct'
    1.65 -    end;
    1.66 -*)
    1.67 +
    1.68 +fun thm'_of_thm thm =
    1.69 +  ((thmID_of_derivation_name o Thm.get_name_hint) thm, string_of_thmI thm): thm'
    1.70  
    1.71  (*.id requested for all, Rls,Seq,Rrls.*)
    1.72  fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)