# HG changeset patch
# User wenzelm
# Date 1010621521 -3600
# Node ID 37cb8f7308f6dfe6c0beb151fdfd655271a688ac
# Parent  9950c1ce9d2414b6fe91b8f1399a7d4d43e6bec4
added hide_thms;

diff -r 9950c1ce9d24 -r 37cb8f7308f6 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Jan 10 01:11:43 2002 +0100
+++ b/src/Pure/pure_thy.ML	Thu Jan 10 01:12:01 2002 +0100
@@ -30,6 +30,7 @@
   val single_thm: string -> thm list -> thm
   val cond_extern_thm_sg: Sign.sg -> string -> xstring
   val thms_containing: theory -> string list -> (string * thm) list
+  val hide_thms: bool -> string list -> theory -> theory
   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
   val smart_store_thms: (bstring * thm list) -> thm list
   val smart_store_thms_open: (bstring * thm list) -> thm list
@@ -221,6 +222,15 @@
 
 (** store theorems **)                    (*DESTRUCTIVE*)
 
+(* hiding -- affects current theory node only! *)
+
+fun hide_thms b names thy =
+  let
+    val r as ref {space, thms_tab, const_idx} = get_theorems thy;
+    val space' = NameSpace.hide b (space, names);
+  in r := {space = space', thms_tab = thms_tab, const_idx = const_idx}; thy end;
+
+
 (* naming *)
 
 fun gen_names j len name =