# HG changeset patch
# User wenzelm
# Date 955973220 -7200
# Node ID ef7efded8fdcedf3e31bd744d6419a9e5808fe1b
# Parent  c7de3c2ed7a94e257cead8ee83f7eabf1263a11d
global/local_path: comment;
added name space hide;

diff -r c7de3c2ed7a9 -r ef7efded8fdc src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Apr 17 14:06:05 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Apr 17 14:07:00 2000 +0200
@@ -19,6 +19,10 @@
   val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_txt_raw: Comment.text -> ProofHistory.T -> ProofHistory.T
+  val global_path: Comment.text -> theory -> theory
+  val local_path: Comment.text -> theory -> theory
+  val hide_space: (string * xstring list) * Comment.text -> theory -> theory
+  val hide_space_i: (string * string list) * Comment.text -> theory -> theory
   val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
   val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
   val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
@@ -190,6 +194,19 @@
 val add_subsubsect = add_txt;
 
 
+(* name spaces *)
+
+fun global_path comment_ignore = PureThy.global_path;
+fun local_path comment_ignore = PureThy.local_path;
+
+fun gen_hide f ((kind, names), comment_ignore) thy =
+  if kind mem_string [Sign.classK, Sign.typeK, Sign.constK] then f (kind, names) thy
+  else error ("Bad name space specification: " ^ quote kind);
+
+val hide_space = gen_hide Theory.hide_space;
+val hide_space_i = gen_hide Theory.hide_space_i;
+
+
 (* signature and syntax *)
 
 val add_classes = Theory.add_classes o Comment.ignore;