tuned;
authorwenzelm
Thu, 11 Oct 2007 16:38:57 +0200
changeset 24973 dc67846b00c0
parent 24972 acafb18a47dc
child 24974 a2f15968a6f2
tuned;
src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Oct 11 16:38:42 2007 +0200
+++ b/src/Pure/sign.ML	Thu Oct 11 16:38:57 2007 +0200
@@ -156,7 +156,7 @@
   val simple_read_term: theory -> typ -> string -> term
   val read_term: theory -> string -> term
   val read_prop: theory -> string -> term
-  val declare_const: Markup.property list -> (bstring * typ * mixfix) -> theory -> term * theory
+  val declare_const: Markup.property list -> bstring * typ * mixfix -> theory -> term * theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val add_abbrev: string -> Markup.property list ->
     bstring * term -> theory -> (term * term) * theory