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