src/Tools/isac/KEStore.thy
changeset 52159 db46e97751eb
parent 52155 e4ddf21390fd
child 52160 112cee0cf30b
     1.1 --- a/src/Tools/isac/KEStore.thy	Fri Oct 25 20:52:08 2013 +0100
     1.2 +++ b/src/Tools/isac/KEStore.thy	Fri Oct 25 20:58:28 2013 +0100
     1.3 @@ -71,20 +71,6 @@
     1.4    | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
     1.5      "TODO exception hierarchy needs to be established.")
     1.6  
     1.7 -(* fun assoc_calc calID = let
     1.8 -    fun ass ([], key) =
     1.9 -          error ("assoc_calc: '"^ key ^"' not found")
    1.10 -      | ass ((calc, (keyi, _)) :: pairs, key) =
    1.11 -          if key = keyi then calc else ass (pairs, key);
    1.12 -  in ass (!calclist', calID) end;
    1.13 -
    1.14 -fun assoc_calc' key' = let
    1.15 -    fun ass ([], key) =
    1.16 -          error ("assoc_calc': '" ^ key ^ "' not found")
    1.17 -      | ass ((all as (keyi, _)) :: pairs, key) =
    1.18 -          if key = keyi then all else ass (pairs, key);
    1.19 -  in ass (!calclist', key') end; *)
    1.20 -
    1.21  fun assoc_calc thy calID = let
    1.22      fun ass ([], key) =
    1.23            error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))