Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorpaulson
Thu, 16 Dec 2010 20:14:21 +0000
changeset 41215 ebeb9424c54b
parent 41213 ee24717e3fe3 (current diff)
parent 41214 8a341cf54a85 (diff)
child 41217 fc9a6d2d7b76
merged
--- 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
isabelle