src/Tools/nbe.ML
changeset 59151 a012574b78e7
parent 59058 a78612c67ec0
child 59153 b5e253703ebd
     1.1 --- a/src/Tools/nbe.ML	Fri Dec 19 12:36:50 2014 +0100
     1.2 +++ b/src/Tools/nbe.ML	Fri Dec 19 12:56:06 2014 +0100
     1.3 @@ -234,18 +234,17 @@
     1.4  structure Univs = Proof_Data
     1.5  (
     1.6    type T = unit -> Univ list -> Univ list
     1.7 -  (* FIXME avoid user error with non-user text *)
     1.8 -  fun init _ () = error "Univs"
     1.9 +  fun init _ () = raise Fail "Univs"
    1.10  );
    1.11  val put_result = Univs.put;
    1.12  
    1.13  local
    1.14 -  val prefix =     "Nbe.";
    1.15 -  val name_put =   prefix ^ "put_result";
    1.16 +  val prefix = "Nbe.";
    1.17 +  val name_put = prefix ^ "put_result";
    1.18    val name_const = prefix ^ "Const";
    1.19 -  val name_abss =  prefix ^ "abss";
    1.20 -  val name_apps =  prefix ^ "apps";
    1.21 -  val name_same =  prefix ^ "same";
    1.22 +  val name_abss = prefix ^ "abss";
    1.23 +  val name_apps = prefix ^ "apps";
    1.24 +  val name_same = prefix ^ "same";
    1.25  in
    1.26  
    1.27  val univs_cookie = (Univs.get, put_result, name_put);