src/HOL/Tools/Datatype/datatype.ML
changeset 35994 9cc3df9a606e
parent 35842 7c170d39a808
child 36148 4ddcc2b07891
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -276,11 +276,11 @@
 
     val _ = message config "Proving isomorphism properties ...";
 
-    val newT_iso_axms = map (fn (_, td) =>
+    val newT_iso_axms = map (fn (_, (_, td)) =>
       (collect_simp (#Abs_inverse td), #Rep_inverse td,
        collect_simp (#Rep td))) typedefs;
 
-    val newT_iso_inj_thms = map (fn (_, td) =>
+    val newT_iso_inj_thms = map (fn (_, (_, td)) =>
       (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs;
 
     (********* isomorphisms between existing types and "unfolded" types *******)