1.1 --- a/src/Tools/isac/Interpret/inform.sml	Tue Nov 19 21:37:18 2013 +0000
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Tue Nov 19 22:18:14 2013 +0000
     1.3 @@ -160,7 +160,7 @@
     1.4  fun cas_input hdt =
     1.5    let val (h,argl) = strip_comb hdt
     1.6    in
     1.7 -    case assoc_castab h of
     1.8 +    case assoc_cas (ML_Context.the_generic_context () |> Context.theory_of) h of
     1.9       NONE => NONE
    1.10     | SOME (spec as (dI,_,_), argl2dtss) =>
    1.11  	      let

     2.1 --- a/src/Tools/isac/KEStore.thy	Tue Nov 19 21:37:18 2013 +0000
     2.2 +++ b/src/Tools/isac/KEStore.thy	Tue Nov 19 22:18:14 2013 +0000
     2.3 @@ -96,11 +96,7 @@
     2.4            if key' = keyi then all else ass (pairs, key');
     2.5    in ass (KEStore_Elems.get_calcs thy, key) end;
     2.6  
     2.7 -fun assoc_cas cas' =
     2.8 -  case AList.lookup (op =) (Thy_Info.get_theory "Isac" |> KEStore_Elems.get_rlss) cas' of
     2.9 -    SOME (_, cas) => cas
    2.10 -  | NONE => raise ERROR ("cas \""^ cas' ^ "\" missing in KEStore.\n" ^
    2.11 -      "TODO exception hierarchy needs to be established.")
    2.12 +fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
    2.13  *}
    2.14  setup {* KEStore_Elems.add_rlss 
    2.15    [("e_rls", (Context.theory_name @{theory}, e_rls)),