# HG changeset patch
# User huffman
# Date 1267419388 28800
# Node ID 7bb9157507a90785a6d9f5682af24288236583b3
# Parent  7a1f285cad256a63f4c2d98208482e5423720292
add_domain_constructors takes iso_info record as argument

diff -r 7a1f285cad25 -r 7bb9157507a9 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Feb 28 19:39:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Feb 28 20:56:28 2010 -0800
@@ -9,9 +9,8 @@
 sig
   val add_domain_constructors :
       string
-      -> typ * (binding * (bool * binding option * typ) list * mixfix) list
-      -> term * term
-      -> thm * thm
+      -> (binding * (bool * binding option * typ) list * mixfix) list
+      -> Domain_Isomorphism.iso_info
       -> thm
       -> theory
       -> { con_consts : term list,
@@ -913,15 +912,17 @@
 
 fun add_domain_constructors
     (dname : string)
-    (lhsT : typ,
-     spec : (binding * (bool * binding option * typ) list * mixfix) list)
-    (rep_const : term, abs_const : term)
-    (rep_iso_thm : thm, abs_iso_thm : thm)
+    (spec : (binding * (bool * binding option * typ) list * mixfix) list)
+    (iso_info : Domain_Isomorphism.iso_info)
     (case_def : thm)
     (thy : theory) =
   let
 
-    (* prove rep/abs strictness rules *)
+    (* retrieve facts about rep/abs *)
+    val lhsT = #absT iso_info;
+    val {rep_const, abs_const, ...} = iso_info;
+    val abs_iso_thm = #abs_inverse iso_info;
+    val rep_iso_thm = #rep_inverse iso_info;
     val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
     val rep_strict = iso_locale RS @{thm iso.rep_strict};
     val abs_strict = iso_locale RS @{thm iso.abs_strict};
diff -r 7a1f285cad25 -r 7bb9157507a9 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 28 19:39:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 28 20:56:28 2010 -0800
@@ -142,10 +142,19 @@
 
 val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
 
+val iso_info : Domain_Isomorphism.iso_info =
+  {
+    absT = lhsT,
+    repT = rhsT,
+    abs_const = abs_const,
+    rep_const = rep_const,
+    abs_inverse = ax_abs_iso,
+    rep_inverse = ax_rep_iso
+  };
+
 val (result, thy) =
   Domain_Constructors.add_domain_constructors
-    (Long_Name.base_name dname) dom_eqn
-    (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) ax_when_def thy;
+    (Long_Name.base_name dname) (snd dom_eqn) iso_info ax_when_def thy;
 
 val con_appls = #con_betas result;
 val {exhaust, casedist, ...} = result;