src/HOLCF/Tools/Domain/domain_take_proofs.ML
changeset 37165 c2e27ae53c2a
parent 37078 a1656804fcad
child 37744 3daaf23b9ab4
     1.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri May 28 17:48:18 2010 +0200
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri May 28 18:15:22 2010 +0200
     1.3 @@ -452,7 +452,7 @@
     1.4  
     1.5      val decisive_lemma =
     1.6        let
     1.7 -        fun iso_locale info =
     1.8 +        fun iso_locale (info : iso_info) =
     1.9              @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info];
    1.10          val iso_locale_thms = map iso_locale iso_infos;
    1.11          val decisive_abs_rep_thms =