# HG changeset patch
# User paulson
# Date 1292530461 0
# Node ID ebeb9424c54b10faa009131eb45b4fd2af895d16
# Parent  ee24717e3fe39e490fb82a2d2a00e072e7b808a5# Parent  8a341cf54a85d127fc76754cb6fe15416af41921
merged

diff -r ee24717e3fe3 -r ebeb9424c54b src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Thu Dec 16 21:02:08 2010 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Thu Dec 16 20:14:21 2010 +0000
@@ -58,7 +58,7 @@
   fun prove_take_apps
       ((dbind, take_const), constr_info) thy =
     let
-      val {iso_info, con_specs, con_betas, ...} = constr_info
+      val {iso_info, con_specs, con_betas, ...} : Domain_Constructors.constr_info = constr_info
       val {abs_inverse, ...} = iso_info
       fun prove_take_app (con_const, args) =
         let
@@ -220,7 +220,7 @@
       val bottoms =
           if length dnames = 1 then ["bottom"] else
           map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
-      fun one_eq bot constr_info =
+      fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
         let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
         in bot :: map name_of (#con_specs constr_info) end
     in adms @ flat (map2 one_eq bottoms constr_infos) end