misc tuning;

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Nov 09 20:47:11 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Nov 09 21:36:18 2011 +0100
@@ -136,9 +136,10 @@
         (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr vs) dTs));
     
     val tycos = map fst dataTs;
-    val _ = if eq_set (op =) (tycos, raw_tycos) then ()
-      else error ("Type constructors " ^ commas (map quote raw_tycos)
-        ^ " do not belong exhaustively to one mutual recursive datatype");
+    val _ =
+      if eq_set (op =) (tycos, raw_tycos) then ()
+      else error ("Type constructors " ^ commas_quote raw_tycos ^
+        " do not belong exhaustively to one mutual recursive datatype");
 
     val (Ts, Us) = (pairself o map) Type protoTs;
 
@@ -406,15 +407,16 @@
       in (tyco, (vs, cT)) end;
 
     val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
-    val _ = case map_filter (fn (tyco, _) =>
-        if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
-     of [] => ()
-      | tycos => error ("Type(s) " ^ commas (map quote tycos)
-          ^ " already represented inductivly");
+    val _ =
+      (case map_filter (fn (tyco, _) =>
+          if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs of
+        [] => ()
+      | tycos => error ("Type(s) " ^ commas_quote tycos ^ " already represented inductivly"));
     val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
-    val ms = case distinct (op =) (map length raw_vss)
-     of [n] => 0 upto n - 1
-      | _ => error ("Different types in given constructors");
+    val ms =
+      (case distinct (op =) (map length raw_vss) of
+         [n] => 0 upto n - 1
+      | _ => error "Different types in given constructors");
     fun inter_sort m = map (fn xs => nth xs m) raw_vss
       |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
     val sorts = map inter_sort ms;

--- a/src/HOL/Tools/transfer.ML	Wed Nov 09 20:47:11 2011 +0100
+++ b/src/HOL/Tools/transfer.ML	Wed Nov 09 21:36:18 2011 +0100
@@ -77,7 +77,7 @@
   let
     val insts = map_filter (fn (k, e) => if exists (member (op =) (#hints e)) hints
       then SOME (direction_of k, transfer_rules_of e) else NONE) (Data.get context);
-    val _ = if null insts then error ("Transfer: no such labels: " ^ commas (map quote hints)) else ();
+    val _ = if null insts then error ("Transfer: no such labels: " ^ commas_quote hints) else ();
   in insts end;
 
 fun splits P [] = []

--- a/src/Pure/Isar/code.ML	Wed Nov 09 20:47:11 2011 +0100
+++ b/src/Pure/Isar/code.ML	Wed Nov 09 21:36:18 2011 +0100
@@ -1174,7 +1174,7 @@
     val (case_const, (k, cos)) = case_cert thm;
     val _ = case filter_out (is_constr thy) cos
      of [] => ()
-      | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
+      | cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs);
     val entry = (1 + Int.max (1, length cos), (k, cos));
     fun register_case cong = (map_cases o apfst)
       (Symtab.update (case_const, (entry, cong)));

--- a/src/Tools/Code/code_runtime.ML	Wed Nov 09 20:47:11 2011 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Nov 09 21:36:18 2011 +0100
@@ -264,11 +264,11 @@
           let
             val missing_constrs = subtract (op =) consts constrs;
             val _ = if null missing_constrs then []
-              else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
+              else error ("Missing constructor(s) " ^ commas_quote missing_constrs
                 ^ " for datatype " ^ quote tyco);
             val false_constrs = subtract (op =) constrs consts;
             val _ = if null false_constrs then []
-              else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
+              else error ("Non-constructor(s) " ^ commas_quote false_constrs
                 ^ " for datatype " ^ quote tyco)
           in () end
       | NONE => ();