diff -r fd58cbf8cae3 -r b8eb7a791dac src/Tools/Code/code_runtime.ML
--- 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 => ();