src/Pure/pure_thy.ML

   val get_thm_closure: theory -> xstring -> thm
   val get_thms_closure: theory -> xstring -> thm list
   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
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm

   |> map (apsnd (Thm.transfer thy));
 
 
 
 (** 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 =
   map (fn i => name ^ "_" ^ string_of_int i) (j+1 upto j+len);