src/HOL/Tools/Datatype/datatype_data.ML
changeset 33969 1e7ca47c6c3d
parent 33968 f94fb13ecbb3
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Nov 30 11:42:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Nov 30 12:28:12 2009 +0100
@@ -101,7 +101,7 @@
 
 fun the_spec thy dtco =
   let
-    val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
+    val { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
     val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
     val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
       o Datatype_Aux.dest_DtTFree) dtys;
@@ -114,7 +114,7 @@
     val info = the_info thy raw_tyco;
     val descr = #descr info;
 
-    val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
+    val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
     val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
       o dest_DtTFree) dtys;