--- 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 => ();