--- a/src/Pure/sign.ML Tue Dec 12 20:49:22 2006 +0100
+++ b/src/Pure/sign.ML Tue Dec 12 20:49:23 2006 +0100
@@ -192,7 +192,7 @@
val read_prop: theory -> string -> term
val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
- val add_abbrev: string -> bstring * term -> theory -> ((string * typ) * term) * theory
+ val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
include SIGN_THEORY
end