--- a/src/HOL/Tools/Datatype/datatype_case.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Mon Dec 12 23:05:21 2011 +0100
@@ -36,10 +36,10 @@
fun ty_info tab sT =
(case tab sT of
- SOME ({descr, case_name, index, sorts, ...} : info) =>
+ SOME ({descr, case_name, index, ...} : info) =>
let
val (_, (tname, dts, constrs)) = nth descr index;
- val mk_ty = Datatype_Aux.typ_of_dtyp descr sorts;
+ val mk_ty = Datatype_Aux.typ_of_dtyp descr;
val T = Type (tname, map mk_ty dts);
in
SOME {case_name = case_name,