# HG changeset patch
# User wenzelm
# Date 1208278166 -7200
# Node ID c95590e01df50c9fe40993e45ca32df464b0d802
# Parent  11f1894911cb3fbd4fd2a15332496aaa5e332509
added hide_names command (formerly Sign.hide_names), support fact name space;

diff -r 11f1894911cb -r c95590e01df5 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Apr 15 18:49:25 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Apr 15 18:49:26 2008 +0200
@@ -22,6 +22,7 @@
   val declaration: string * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> string * Position.T -> string list ->
     local_theory -> local_theory
+  val hide_names: bool -> string * xstring list -> theory -> theory
   val have: ((string * Attrib.src list) * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
   val hence: ((string * Attrib.src list) * (string * string list) list) list ->
@@ -252,6 +253,27 @@
   |> Context.proof_map;
 
 
+(* hide names *)
+
+val hide_kinds =
+ [("class", (Sign.intern_class, can o Sign.certify_class, Sign.hide_class)),
+  ("type", (Sign.intern_type, Sign.declared_tyname, Sign.hide_type)),
+  ("const", (Sign.intern_const, Sign.declared_const, Sign.hide_const)),
+  ("fact", (PureThy.intern_fact, PureThy.check_fact, PureThy.hide_fact))];
+
+fun hide_names b (kind, xnames) thy =
+  (case AList.lookup (op =) hide_kinds kind of
+    SOME (intern, check, hide) =>
+      let
+        val names = map (intern thy) xnames;
+        val bads = filter_out (check thy) names;
+      in
+        if null bads then fold (hide b) names thy
+        else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
+      end
+  | NONE => error ("Bad name space specification: " ^ quote kind));
+
+
 (* goals *)
 
 fun goal opt_chain goal stmt int =