1.1 --- a/src/Tools/isac/CalcElements/thmC.sml	Thu Apr 09 18:21:09 2020 +0200
     1.2 +++ b/src/Tools/isac/CalcElements/thmC.sml	Fri Apr 10 12:28:47 2020 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val thmID_of_derivation_name: string -> string
     1.5    val thmID_of_derivation_name': thm -> string
     1.6    val thm''_of_thm: thm -> thm''
     1.7 -  val thm_of_thm: Rule.rule -> thm
     1.8 +  val thm_of_thm: Rule_Def.rule -> thm
     1.9  
    1.10    val string_of_thmI: thm -> string
    1.11  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.12 @@ -28,7 +28,7 @@
    1.13    val string_of_thm': theory -> thm -> string
    1.14  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.15  (*/------- to ThmC.sml ------\*)
    1.16 -    val id_of_thm: Rule.rule -> string
    1.17 +    val id_of_thm: Rule_Def.rule -> string
    1.18  (*\------- to ThmC.sml ------/*)
    1.19  end
    1.20  
    1.21 @@ -84,13 +84,13 @@
    1.22      | _ => str
    1.23    end
    1.24  
    1.25 -fun id_of_thm (Rule.Thm (id, _)) = id  (* TODO re-arrange code for rule2str *)
    1.26 +fun id_of_thm (Rule_Def.Thm (id, _)) = id  (* TODO re-arrange code for rule2str *)
    1.27    | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
    1.28  
    1.29  fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
    1.30  fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
    1.31  fun thyID_of_derivation_name dn = hd (space_explode "." dn);
    1.32 -fun thm_of_thm (Rule.Thm (_, thm)) = thm  (* TODO re-arrange code for rule2str *)
    1.33 +fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm  (* TODO re-arrange code for rule2str *)
    1.34    | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
    1.35  fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
    1.36