# HG changeset patch
# User haftmann
# Date 1250257017 -7200
# Node ID 62617ef2c0d0dee0153871c25c6220dcb2e431b6
# Parent  c96330408d8910a9aa54bdc7b88773580dd7f2c4
inserted space into message

diff -r c96330408d89 -r 62617ef2c0d0 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Aug 14 15:36:55 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Aug 14 15:36:57 2009 +0200
@@ -119,7 +119,7 @@
     val tycos = map fst dataTs;
     val _ = if gen_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");
+        ^ " do not belong exhaustively to one mutual recursive datatype");
 
     val (Ts, Us) = (pairself o map) Type protoTs;