1.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Jun 22 14:58:51 2014 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Sun Jun 22 15:17:07 2014 +0200
     1.3 @@ -87,10 +87,6 @@
     1.4  *}
     1.5  subsection {* (0) Survey on remaining Unsynchronized.ref *}
     1.6  text {*
     1.7 -  REMOVE WITHOUT REPLACEMENT (requires some efforts)
     1.8 -    calcelems.sml:val theory'  = Unsynchronized.ref ([]:(theory' * theory) list);
     1.9 -    calcelems.sml:val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list);
    1.10 -    calcelems.sml:val isabthys = Unsynchronized.ref ([] : theory list);
    1.11    REPLACE BY KEStore... (has been overlooked)
    1.12      calcelems.sml:val rew_ord' = Unsynchronized.ref ...
    1.13    KEEP FOR TRACING

     2.1 --- a/src/Tools/isac/calcelems.sml	Sun Jun 22 14:58:51 2014 +0200
     2.2 +++ b/src/Tools/isac/calcelems.sml	Sun Jun 22 15:17:07 2014 +0200
     2.3 @@ -547,13 +547,6 @@
     2.4      end
     2.5    | n => error ("theID2guh called with theID = " ^ strs2str' theID);
     2.6  
     2.7 -(* an association list, gets the value once in Isac.ML.
     2.8 -   stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
     2.9 -   WN1-1-28 make this data arguments and del ref ?*)
    2.10 -val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list);
    2.11 -val isabthys = Unsynchronized.ref ([] : theory list);
    2.12 -
    2.13 -
    2.14  type path = string;
    2.15  type filename = string;
    2.16  
    2.17 @@ -699,8 +692,6 @@
    2.18    | assoc' ((keyi, xi) :: pairs, key) =
    2.19        if key = keyi then SOME xi else assoc' (pairs, key);
    2.20  
    2.21 -(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
    2.22 -  handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
    2.23  fun assoc_thy (thy:theory') =
    2.24      if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
    2.25      else (Thy_Info.get_theory thy)