src/Pure/defs.ML
changeset 17711 c16cbe73798c
parent 17707 bc0270e9d27f
child 17712 46c2091e5187
     1.1 --- a/src/Pure/defs.ML	Thu Sep 29 00:59:03 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Sep 29 01:09:39 2005 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val merge: Pretty.pp -> T * T -> T
     1.5  end
     1.6  
     1.7 -structure Defs (* FIXME : DEFS *) =
     1.8 +structure Defs: DEFS =
     1.9  struct
    1.10  
    1.11  (** datatype T **)