diff -r a8455ca995d6 -r eb59c9b76d52 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Apr 26 14:24:13 2007 +0200
+++ b/src/Pure/sign.ML	Thu Apr 26 14:24:14 2007 +0200
@@ -23,11 +23,6 @@
   val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
   val add_consts: (bstring * string * mixfix) list -> theory -> theory
   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
-  val add_const_constraint: xstring * string option -> theory -> theory
-  val add_const_constraint_i: string * typ option -> theory -> theory
-  val primitive_class: string * class list -> theory -> theory
-  val primitive_classrel: class * class -> theory -> theory
-  val primitive_arity: arity -> theory -> theory
   val add_trfuns:
     (string * (ast list -> ast)) list *
     (string * (term list -> term)) list *
@@ -178,6 +173,11 @@
   val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
   val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
   include SIGN_THEORY
+  val add_const_constraint: xstring * string option -> theory -> theory
+  val add_const_constraint_i: string * typ option -> theory -> theory
+  val primitive_class: string * class list -> theory -> theory
+  val primitive_classrel: class * class -> theory -> theory
+  val primitive_arity: arity -> theory -> theory
   val hide_classes: bool -> xstring list -> theory -> theory
   val hide_classes_i: bool -> string list -> theory -> theory
   val hide_types: bool -> xstring list -> theory -> theory