made sml/nj happy
authorpaulson
Thu Dec 16 20:14:04 2010 +0000 (2010-12-16 ago)
changeset 412148a341cf54a85
parent 41194 9796e5e01b61
child 41215 ebeb9424c54b
made sml/nj happy
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Thu Dec 16 12:19:00 2010 +0000
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Thu Dec 16 20:14:04 2010 +0000
     1.3 @@ -58,7 +58,7 @@
     1.4    fun prove_take_apps
     1.5        ((dbind, take_const), constr_info) thy =
     1.6      let
     1.7 -      val {iso_info, con_specs, con_betas, ...} = constr_info
     1.8 +      val {iso_info, con_specs, con_betas, ...} : Domain_Constructors.constr_info = constr_info
     1.9        val {abs_inverse, ...} = iso_info
    1.10        fun prove_take_app (con_const, args) =
    1.11          let
    1.12 @@ -220,7 +220,7 @@
    1.13        val bottoms =
    1.14            if length dnames = 1 then ["bottom"] else
    1.15            map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
    1.16 -      fun one_eq bot constr_info =
    1.17 +      fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
    1.18          let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
    1.19          in bot :: map name_of (#con_specs constr_info) end
    1.20      in adms @ flat (map2 one_eq bottoms constr_infos) end