diff -r 9a13e0abdb82 -r c16cbe73798c src/Pure/defs.ML
--- a/src/Pure/defs.ML	Thu Sep 29 00:59:03 2005 +0200
+++ b/src/Pure/defs.ML	Thu Sep 29 01:09:39 2005 +0200
@@ -15,7 +15,7 @@
   val merge: Pretty.pp -> T * T -> T
 end
 
-structure Defs (* FIXME : DEFS *) =
+structure Defs: DEFS =
 struct
 
 (** datatype T **)