# HG changeset patch
# User blanchet
# Date 1292530912 -3600
# Node ID fc9a6d2d7b760812a09a891590262c2483ae03c5
# Parent  5cee84180cd77162ea727e85f73d16d319018fbc# Parent  ebeb9424c54b10faa009131eb45b4fd2af895d16
merge

diff -r 5cee84180cd7 -r fc9a6d2d7b76 src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Thu Dec 16 21:21:13 2010 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Thu Dec 16 21:21:52 2010 +0100
@@ -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