add_abbrev: tuned signature;
authorwenzelm
Tue Dec 12 20:49:23 2006 +0100 (2006-12-12)
changeset 21796481094a3dd1f
parent 21795 d7dcc3dfa7e9
child 21797 25b97f5057f2
add_abbrev: tuned signature;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Dec 12 20:49:22 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Dec 12 20:49:23 2006 +0100
     1.3 @@ -192,7 +192,7 @@
     1.4    val read_prop: theory -> string -> term
     1.5    val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
     1.6    val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
     1.7 -  val add_abbrev: string -> bstring * term -> theory -> ((string * typ) * term) * theory
     1.8 +  val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
     1.9    include SIGN_THEORY
    1.10  end
    1.11