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