src/Pure/sign.ML
changeset 22796 34c316d7b630
parent 22765 2a3840aa2ffd
child 22811 eb59c9b76d52
--- 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 =