pass binding as argument to add_domain_constructors; proper binding for case combinator

--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Mar 13 16:48:57 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Mar 13 17:05:34 2010 -0800
@@ -8,7 +8,7 @@
 signature DOMAIN_CONSTRUCTORS =
 sig
   val add_domain_constructors :
-      string
+      binding
       -> (binding * (bool * binding option * typ) list * mixfix) list
       -> Domain_Take_Proofs.iso_info
       -> theory
@@ -367,7 +367,7 @@
 fun add_case_combinator
     (spec : (term * (bool * typ) list) list)
     (lhsT : typ)
-    (dname : string)
+    (dbind : binding)
     (con_betas : thm list)
     (casedist : thm)
     (iso_locale : thm)
@@ -420,7 +420,7 @@
 
     (* definition of case combinator *)
     local
-      val case_bind = Binding.name (dname ^ "_when");
+      val case_bind = Binding.suffix_name "_when" dbind;
       fun one_con f (_, args) =
         let
           fun argT (lazy, T) = if lazy then mk_upT T else T;
@@ -1011,11 +1011,12 @@
 (******************************************************************************)
 
 fun add_domain_constructors
-    (dname : string)
+    (dbind : binding)
     (spec : (binding * (bool * binding option * typ) list * mixfix) list)
     (iso_info : Domain_Take_Proofs.iso_info)
     (thy : theory) =
   let
+    val dname = Binding.name_of dbind;
 
     (* retrieve facts about rep/abs *)
     val lhsT = #absT iso_info;
@@ -1049,7 +1050,7 @@
         fun prep_con c (b, args, mx) = (c, map prep_arg args);
         val case_spec = map2 prep_con con_consts spec;
       in
-        add_case_combinator case_spec lhsT dname
+        add_case_combinator case_spec lhsT dbind
           con_betas casedist iso_locale rep_const thy
       end;
 

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 16:48:57 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 17:05:34 2010 -0800
@@ -115,8 +115,7 @@
 (* ----- define constructors ------------------------------------------------ *)
 
 val (result, thy) =
-  Domain_Constructors.add_domain_constructors
-    (Long_Name.base_name dname) spec iso_info thy;
+    Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
 
 val con_appls = #con_betas result;
 val {exhaust, casedist, ...} = result;