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))