inserted space into message
authorhaftmann
Fri Aug 14 15:36:57 2009 +0200 (2009-08-14)
changeset 3237462617ef2c0d0
parent 32373 c96330408d89
child 32375 d33f5a96df0b
inserted space into message
src/HOL/Tools/Datatype/datatype.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Aug 14 15:36:55 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Aug 14 15:36:57 2009 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4      val tycos = map fst dataTs;
     1.5      val _ = if gen_eq_set (op =) (tycos, raw_tycos) then ()
     1.6        else error ("Type constructors " ^ commas (map quote raw_tycos)
     1.7 -        ^ "do not belong exhaustively to one mutual recursive datatype");
     1.8 +        ^ " do not belong exhaustively to one mutual recursive datatype");
     1.9  
    1.10      val (Ts, Us) = (pairself o map) Type protoTs;
    1.11