src/Tools/nbe.ML
changeset 41472 f6ab14e61604
parent 41346 6673f6fa94ca
child 42361 23f352990944
     1.1 --- a/src/Tools/nbe.ML	Sat Jan 08 16:01:51 2011 +0100
     1.2 +++ b/src/Tools/nbe.ML	Sat Jan 08 17:14:48 2011 +0100
     1.3 @@ -229,8 +229,10 @@
     1.4  
     1.5  (* nbe specific syntax and sandbox communication *)
     1.6  
     1.7 -structure Univs = Proof_Data (
     1.8 +structure Univs = Proof_Data
     1.9 +(
    1.10    type T = unit -> Univ list -> Univ list
    1.11 +  (* FIXME avoid user error with non-user text *)
    1.12    fun init _ () = error "Univs"
    1.13  );
    1.14  val put_result = Univs.put;