diff -r c16cbe73798c -r 46c2091e5187 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Thu Sep 29 01:09:39 2005 +0200
+++ b/src/Pure/defs.ML	Thu Sep 29 01:12:16 2005 +0200
@@ -10,7 +10,7 @@
 sig
   type T
   val monomorphic: T -> string -> bool
-  val define: string -> string * typ -> (string * typ) list -> T -> T
+  val define: (string -> typ) -> string -> string * typ -> (string * typ) list -> T -> T
   val empty: T
   val merge: Pretty.pp -> T * T -> T
 end