src/Pure/sign.ML
changeset 21796 481094a3dd1f
parent 21772 7c7ade4f537b
child 21932 7d592dc078e3
     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