# HG changeset patch
# User wenzelm
# Date 1127948979 -7200
# Node ID c16cbe73798c6f5468295cacfd71c5690823fba1
# Parent  9a13e0abdb8275e652607b1894ab9c7b121777ed
activate signature constraints;

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 **)