diff -r 702542e7f88c -r 34c316d7b630 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/sign.ML	Thu Apr 26 12:00:05 2007 +0200
@@ -61,14 +61,6 @@
   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
     theory -> theory
   val restore_naming: theory -> 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
-  val hide_types_i: bool -> string list -> theory -> theory
-  val hide_consts: bool -> xstring list -> theory -> theory
-  val hide_consts_i: bool -> string list -> theory -> theory
-  val hide_names: bool -> string * xstring list -> theory -> theory
-  val hide_names_i: bool -> string * string list -> theory -> theory
 end
 
 signature SIGN =
@@ -186,6 +178,14 @@
   val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
   val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
   include SIGN_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
+  val hide_types_i: bool -> string list -> theory -> theory
+  val hide_consts: bool -> xstring list -> theory -> theory
+  val hide_consts_i: bool -> string list -> theory -> theory
+  val hide_names: bool -> string * xstring list -> theory -> theory
+  val hide_names_i: bool -> string * string list -> theory -> theory
 end
 
 structure Sign: SIGN =