src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 40014 7469b323e260
parent 40013 9db8fb58fddc
child 40016 2eff1cbc1ccb
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 09:34:00 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 09:44:40 2010 -0700
     1.3 @@ -106,7 +106,7 @@
     1.4      (((dname, _), cons) : eq, eqs : eq list)
     1.5      (iso_info : Domain_Take_Proofs.iso_info)
     1.6      (take_info : Domain_Take_Proofs.take_induct_info)
     1.7 -    (result)
     1.8 +    (result : Domain_Constructors.constr_info)
     1.9      (thy : theory) =
    1.10  let
    1.11    val map_tab = Domain_Take_Proofs.get_map_tab thy;