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