# HG changeset patch
# User huffman
# Date 1287888993 25200
# Node ID 429cd74f795f8781d660863204f3b1a2fda0097e
# Parent  4d1a8fa8cdfd09eeffdc8ea768ed3986cfd79bba
remove legacy comp_dbind option from domain package

diff -r 4d1a8fa8cdfd -r 429cd74f795f src/HOLCF/Tools/Domain/domain.ML
--- a/src/HOLCF/Tools/Domain/domain.ML	Sat Oct 23 11:04:26 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain.ML	Sat Oct 23 19:56:33 2010 -0700
@@ -8,25 +8,21 @@
 signature DOMAIN =
 sig
   val add_domain_cmd:
-      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * string) list * mixfix) list) list
       -> theory -> theory
 
   val add_domain:
-      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * typ) list * mixfix) list) list
       -> theory -> theory
 
   val add_new_domain_cmd:
-      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * string) list * mixfix) list) list
       -> theory -> theory
 
   val add_new_domain:
-      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * typ) list * mixfix) list) list
       -> theory -> theory
@@ -50,7 +46,6 @@
     (prep_typ : theory -> (string * sort) list -> 'a -> typ)
     (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
     (arg_sort : bool -> sort)
-    (comp_dbind : binding)
     (raw_specs : ((string * string option) list * binding * mixfix *
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
     (thy : theory) =
@@ -172,7 +167,7 @@
              (dbinds ~~ rhss ~~ iso_infos);
 
     val (take_rews, thy) =
-        Domain_Induction.comp_theorems comp_dbind
+        Domain_Induction.comp_theorems
           dbinds take_info constr_infos thy;
   in
     thy
@@ -240,27 +235,21 @@
     (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
 
 val domains_decl =
-  Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
-    Parse.and_list1 domain_decl;
+  Parse.and_list1 domain_decl;
 
 fun mk_domain
     (definitional : bool)
-    (opt_name : binding option,
-     doms : ((((string * string option) list * binding) * mixfix) *
+    (doms : ((((string * string option) list * binding) * mixfix) *
              ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
   let
-    val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
     val specs : ((string * string option) list * binding * mixfix *
                  (binding * (bool * binding option * string) list * mixfix) list) list =
         map (fn (((vs, t), mx), cons) =>
                 (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
-    val comp_dbind =
-        case opt_name of NONE => Binding.name (space_implode "_" names)
-                       | SOME s => s;
   in
-    if definitional 
-    then add_new_domain_cmd comp_dbind specs
-    else add_domain_cmd comp_dbind specs
+    if definitional
+    then add_new_domain_cmd specs
+    else add_domain_cmd specs
   end;
 
 val _ =
diff -r 4d1a8fa8cdfd -r 429cd74f795f src/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOLCF/Tools/Domain/domain_induction.ML	Sat Oct 23 11:04:26 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_induction.ML	Sat Oct 23 19:56:33 2010 -0700
@@ -8,7 +8,7 @@
 signature DOMAIN_INDUCTION =
 sig
   val comp_theorems :
-      binding -> binding list ->
+      binding list ->
       Domain_Take_Proofs.take_induct_info ->
       Domain_Constructors.constr_info list ->
       theory -> thm list * theory
@@ -367,13 +367,14 @@
 (******************************************************************************)
 
 fun comp_theorems
-    (comp_dbind : binding)
     (dbinds : binding list)
     (take_info : Domain_Take_Proofs.take_induct_info)
     (constr_infos : Domain_Constructors.constr_info list)
     (thy : theory) =
 let
-val comp_dname = Binding.name_of comp_dbind;
+
+val comp_dname = space_implode "_" (map Binding.name_of dbinds);
+val comp_dbind = Binding.name comp_dname;
 
 (* Test for emptiness *)
 (* FIXME: reimplement emptiness test