tuned whitespace
authorhaftmann
Tue, 07 Dec 2010 21:32:47 +0100
changeset 413167e643e07be7f
parent 41315 c78a2d402736
child 41319 7204024077a8
tuned whitespace
src/Tools/nbe.ML
     1.1 --- a/src/Tools/nbe.ML	Tue Dec 07 17:23:14 2010 +0100
     1.2 +++ b/src/Tools/nbe.ML	Tue Dec 07 21:32:47 2010 +0100
     1.3 @@ -235,13 +235,13 @@
     1.4  val put_result = Univs.put;
     1.5  
     1.6  local
     1.7 -  val prefix =      "Nbe.";
     1.8 -  val name_put =    prefix ^ "put_result";
     1.9 -  val name_ref =    prefix ^ "univs_ref";
    1.10 -  val name_const =  prefix ^ "Const";
    1.11 -  val name_abss =   prefix ^ "abss";
    1.12 -  val name_apps =   prefix ^ "apps";
    1.13 -  val name_same =     prefix ^ "same";
    1.14 +  val prefix =     "Nbe.";
    1.15 +  val name_put =   prefix ^ "put_result";
    1.16 +  val name_ref =   prefix ^ "univs_ref";
    1.17 +  val name_const = prefix ^ "Const";
    1.18 +  val name_abss =  prefix ^ "abss";
    1.19 +  val name_apps =  prefix ^ "apps";
    1.20 +  val name_same =  prefix ^ "same";
    1.21  in
    1.22  
    1.23  val univs_cookie = (Univs.get, put_result, name_put);