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);