# HG changeset patch
# User wenzelm
# Date 1165952963 -3600
# Node ID 481094a3dd1f2e77a27bd0792a1687d709d3bf99
# Parent  d7dcc3dfa7e9ceb948d5fec8126df28afb4eb30c
add_abbrev: tuned signature;

diff -r d7dcc3dfa7e9 -r 481094a3dd1f src/Pure/sign.ML
--- 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