make signature constraint actually work;
authorwenzelm
Thu Sep 29 01:12:16 2005 +0200 (2005-09-29)
changeset 1771246c2091e5187
parent 17711 c16cbe73798c
child 17713 7efbe0ec9d4c
make signature constraint actually work;
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Thu Sep 29 01:09:39 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Sep 29 01:12:16 2005 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  sig
     1.5    type T
     1.6    val monomorphic: T -> string -> bool
     1.7 -  val define: string -> string * typ -> (string * typ) list -> T -> T
     1.8 +  val define: (string -> typ) -> string -> string * typ -> (string * typ) list -> T -> T
     1.9    val empty: T
    1.10    val merge: Pretty.pp -> T * T -> T
    1.11  end