src/Tools/nbe.ML
changeset 41068 7e643e07be7f
parent 41037 6d6f23b3a879
child 41100 6c0940392fb4
     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);