# HG changeset patch
# User haftmann
# Date 1255514656 -7200
# Node ID 342d89e5a808c1b96d3730ecf67c7dd3635b6a3a
# Parent  980f5aa0d2d727ecf2113738e96235dd6c57bbe7
tuned whitespace

diff -r 980f5aa0d2d7 -r 342d89e5a808 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Wed Oct 14 12:03:16 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Wed Oct 14 12:04:16 2009 +0200
@@ -529,7 +529,7 @@
                     val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
                     val vars = reserved
                       |> intro_base_names
-                      (is_none o syntax_const) deresolve consts;
+                          (is_none o syntax_const) deresolve consts;
                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (