src/HOL/Tools/datatype_rep_proofs.ML
changeset 18330 444f16d232a2
parent 18314 4595eb4627fa
child 18358 0a733e11021a
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 01 22:43:15 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Dec 02 08:06:59 2005 +0100
     1.3 @@ -505,8 +505,8 @@
     1.4  
     1.5      val Abs_inverse_thms' =
     1.6        map #1 newT_iso_axms @
     1.7 -      map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp])
     1.8 -        (iso_inj_thms_unfolded, iso_thms);
     1.9 +      map2 (fn r_inj => fn r => f_myinv_f OF [r_inj, r RS mp])
    1.10 +        iso_inj_thms_unfolded iso_thms;
    1.11  
    1.12      val Abs_inverse_thms = List.concat (map mk_funs_inv Abs_inverse_thms');
    1.13