inserted space into message
authorhaftmann
Fri, 14 Aug 2009 15:36:57 +0200
changeset 32374 62617ef2c0d0
parent 32373 c96330408d89
child 32375 d33f5a96df0b
inserted space into message
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;