# HG changeset patch
# User wenzelm
# Date 1460925530 -7200
# Node ID 89d19aa73081a487d42f8d96dbb592aa95e550d9
# Parent  d743bb1b6c23461ecc024ab54d6f187d7fe55612
clarified bindings;

diff -r d743bb1b6c23 -r 89d19aa73081 src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Apr 17 22:10:09 2016 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Apr 17 22:38:50 2016 +0200
@@ -375,8 +375,8 @@
     (thy : theory) =
 let
 
-val comp_dname = space_implode "_" (map Binding.name_of dbinds)
-val comp_dbind = Binding.name comp_dname
+val comp_dbind = Binding.conglomerate dbinds
+val comp_dname = Binding.name_of comp_dbind
 
 (* Test for emptiness *)
 (* FIXME: reimplement emptiness test
diff -r d743bb1b6c23 -r 89d19aa73081 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sun Apr 17 22:10:09 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Apr 17 22:38:50 2016 +0200
@@ -78,11 +78,7 @@
     val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
 
     val fnames = map (fst o fst) fixes0
-    val f_base_names = map (fst o fst) fixes
-    val defname =
-      (case fixes0 of
-        [((b, _), _)] => b
-      | _ => Binding.name (space_implode "_" f_base_names))
+    val defname = Binding.conglomerate fnames;
 
     val FunctionConfig {partials, default, ...} = config
     val _ =
diff -r d743bb1b6c23 -r 89d19aa73081 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Apr 17 22:10:09 2016 +0200
+++ b/src/HOL/Tools/inductive.ML	Sun Apr 17 22:38:50 2016 +0200
@@ -842,11 +842,7 @@
     val is_auxiliary = length cs > 1;
 
     val rec_binding =
-      if Binding.is_empty alt_name then
-        (case cnames_syn of
-          [(b, _)] => b
-        | _ => Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn)))
-      else alt_name;
+      if Binding.is_empty alt_name then Binding.conglomerate (map #1 cnames_syn) else alt_name;
     val rec_name = Binding.name_of rec_binding;
 
     val internals = Config.get lthy inductive_internals;
diff -r d743bb1b6c23 -r 89d19aa73081 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sun Apr 17 22:10:09 2016 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Sun Apr 17 22:38:50 2016 +0200
@@ -495,9 +495,7 @@
 
     (* convert theorems to set notation *)
     val rec_name =
-      if Binding.is_empty alt_name then
-        Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
-      else alt_name;
+      if Binding.is_empty alt_name then Binding.conglomerate (map #1 cnames_syn) else alt_name;
     val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
     val (intr_names, intr_atts) = split_list (map fst intros);
     val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
diff -r d743bb1b6c23 -r 89d19aa73081 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Sun Apr 17 22:10:09 2016 +0200
+++ b/src/Pure/General/binding.ML	Sun Apr 17 22:38:50 2016 +0200
@@ -25,6 +25,7 @@
   val eq_name: binding * binding -> bool
   val empty: binding
   val is_empty: binding -> bool
+  val conglomerate: binding list -> binding
   val qualify: bool -> string -> binding -> binding
   val qualify_name: bool -> binding -> string -> binding
   val qualified_name: string -> binding
@@ -101,6 +102,9 @@
 val empty = name "";
 fun is_empty b = name_of b = "";
 
+fun conglomerate [b] = b
+  | conglomerate bs = name (space_implode "_" (map name_of bs));
+
 
 (* user qualifier *)