# HG changeset patch
# User haftmann
# Date 1284617914 -7200
# Node ID 4a7d09da2b9c02b567724669e27117a5c6da971c
# Parent  5d18f4c00c07af421bce618547fdaea1b78fa5e4
tuned whitespace

diff -r 5d18f4c00c07 -r 4a7d09da2b9c src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Sep 16 06:49:46 2010 +0200
+++ b/src/Tools/nbe.ML	Thu Sep 16 08:18:34 2010 +0200
@@ -555,6 +555,7 @@
     |> traced (fn _ => "---\n")
   end;
 
+
 (* function store *)
 
 structure Nbe_Functions = Code_Data