# HG changeset patch
# User paulson
# Date 1138612408 -3600
# Node ID afe45058241aabe6c0a0ad5720ad6ce03b09caae
# Parent  f1e2602ca7bac8e1b6a9e27756ae60bbbaeaf493
fixed a syntax error!

diff -r f1e2602ca7ba -r afe45058241a src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Mon Jan 30 08:47:38 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Jan 30 10:13:28 2006 +0100
@@ -324,7 +324,7 @@
        of (es, IConst (c, _)) =>
             if c = thingol_nil
             then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es))
-            else pretty_default fxy pr e1 e2)
+            else pretty_default fxy pr e1 e2
         | _ => pretty_default fxy pr e1 e2;
   in ((2, 2), pretty_compact) end;