# HG changeset patch
# User haftmann
# Date 1291753967 -3600
# Node ID 7e643e07be7f57f67a11952b3c68f78ab32d8940
# Parent  c78a2d402736ee3339a721376c13b67055a0980b
tuned whitespace

diff -r c78a2d402736 -r 7e643e07be7f src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Dec 07 17:23:14 2010 +0100
+++ b/src/Tools/nbe.ML	Tue Dec 07 21:32:47 2010 +0100
@@ -235,13 +235,13 @@
 val put_result = Univs.put;
 
 local
-  val prefix =      "Nbe.";
-  val name_put =    prefix ^ "put_result";
-  val name_ref =    prefix ^ "univs_ref";
-  val name_const =  prefix ^ "Const";
-  val name_abss =   prefix ^ "abss";
-  val name_apps =   prefix ^ "apps";
-  val name_same =     prefix ^ "same";
+  val prefix =     "Nbe.";
+  val name_put =   prefix ^ "put_result";
+  val name_ref =   prefix ^ "univs_ref";
+  val name_const = prefix ^ "Const";
+  val name_abss =  prefix ^ "abss";
+  val name_apps =  prefix ^ "apps";
+  val name_same =  prefix ^ "same";
 in
 
 val univs_cookie = (Univs.get, put_result, name_put);