# HG changeset patch
# User haftmann
# Date 1234981112 -3600
# Node ID cbf46080ea3a0f7bb46c37307e7176788649ec00
# Parent  9dbb046136d0aeb00d51a71784e8415c85b46d20
tuned accessor name

diff -r 9dbb046136d0 -r cbf46080ea3a src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Feb 18 19:18:32 2009 +0100
+++ b/src/Pure/Isar/code.ML	Wed Feb 18 19:18:32 2009 +0100
@@ -35,7 +35,7 @@
   val these_raw_eqns: theory -> string -> (thm * bool) list
   val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
   val get_datatype_of_constr: theory -> string -> string option
-  val get_case_data: theory -> string -> (int * string list) option
+  val get_case_scheme: theory -> string -> (int * string list) option
   val is_undefined: theory -> string -> bool
   val default_typscheme: theory -> string -> (string * sort) list * typ
 
@@ -583,7 +583,7 @@
 
 fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
 
-val get_case_data = Symtab.lookup o fst o the_cases o the_exec;
+fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
 
 val is_undefined = Symtab.defined o snd o the_cases o the_exec;