# HG changeset patch
# User huffman
# Date 1268601036 25200
# Node ID 48cd2261817ba097117bf107ac541edcd87e278d
# Parent  dc175fe29326321796d6f3b7e5974e2612d6c566
old domain package also defines map functions

diff -r dc175fe29326 -r 48cd2261817b src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Sun Mar 14 14:10:05 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Sun Mar 14 14:10:36 2010 -0700
@@ -119,6 +119,11 @@
         Domain_Take_Proofs.add_lub_take_theorems
           (map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy;
 
+    (* define map functions *)
+    val (map_info, thy) =
+        Domain_Isomorphism.define_map_functions
+          (map fst dom_eqns ~~ iso_infos) thy;
+
   in
     ((iso_infos, take_info2), thy)
   end;