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