tuned accessor name
authorhaftmann
Wed, 18 Feb 2009 19:18:32 +0100
changeset 29970 cbf46080ea3a
parent 29969 9dbb046136d0
child 29971 68331b62c873
tuned accessor name
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;