1.1 --- a/src/Pure/Isar/code.ML	Wed Feb 18 19:18:32 2009 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Feb 18 19:18:32 2009 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4    val these_raw_eqns: theory -> string -> (thm * bool) list
     1.5    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
     1.6    val get_datatype_of_constr: theory -> string -> string option
     1.7 -  val get_case_data: theory -> string -> (int * string list) option
     1.8 +  val get_case_scheme: theory -> string -> (int * string list) option
     1.9    val is_undefined: theory -> string -> bool
    1.10    val default_typscheme: theory -> string -> (string * sort) list * typ
    1.11  
    1.12 @@ -583,7 +583,7 @@
    1.13  
    1.14  fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
    1.15  
    1.16 -val get_case_data = Symtab.lookup o fst o the_cases o the_exec;
    1.17 +fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
    1.18  
    1.19  val is_undefined = Symtab.defined o snd o the_cases o the_exec;
    1.20