more direct access to naming;
tuned signature;

--- a/src/Pure/Isar/proof.ML	Sun Oct 25 19:14:46 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Oct 25 19:17:42 2009 +0100
@@ -162,7 +162,8 @@
   make_node (f (context, facts, mode, goal));
 
 val init_context =
-  ProofContext.set_stmt true #> ProofContext.reset_naming;
+  ProofContext.set_stmt true #>
+  ProofContext.map_naming (K ProofContext.local_naming);
 
 fun init ctxt =
   State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));

--- a/src/Pure/Isar/proof_context.ML	Sun Oct 25 19:14:46 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Oct 25 19:17:42 2009 +0100
@@ -21,7 +21,10 @@
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
+  val local_naming: Name_Space.naming
+  val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
   val naming_of: Proof.context -> Name_Space.naming
+  val restore_naming: Proof.context -> Proof.context -> Proof.context
   val full_name: Proof.context -> binding -> string
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
@@ -92,11 +95,6 @@
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
-  val add_path: string -> Proof.context -> Proof.context
-  val mandatory_path: string -> Proof.context -> Proof.context
-  val conceal: Proof.context -> Proof.context
-  val restore_naming: Proof.context -> Proof.context -> Proof.context
-  val reset_naming: Proof.context -> Proof.context
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
@@ -232,6 +230,7 @@
   map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
 
 val naming_of = #naming o rep_context;
+val restore_naming = map_naming o K o naming_of
 val full_name = Name_Space.full_name o naming_of;
 
 val syntax_of = #syntax o rep_context;
@@ -923,15 +922,6 @@
 end;
 
 
-(* name space operations *)
-
-val add_path = map_naming o Name_Space.add_path;
-val mandatory_path = map_naming o Name_Space.mandatory_path;
-val conceal = map_naming Name_Space.conceal;
-val restore_naming = map_naming o K o naming_of;
-val reset_naming = map_naming (K local_naming);
-
-
 (* facts *)
 
 local

--- a/src/Pure/sign.ML	Sun Oct 25 19:14:46 2009 +0100
+++ b/src/Pure/sign.ML	Sun Oct 25 19:17:42 2009 +0100
@@ -12,6 +12,7 @@
     syn: Syntax.syntax,
     tsig: Type.tsig,
     consts: Consts.T}
+  val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
   val naming_of: theory -> Name_Space.naming
   val full_name: theory -> binding -> string
   val full_name_path: theory -> string -> binding -> string
@@ -125,7 +126,6 @@
   val parent_path: theory -> theory
   val mandatory_path: string -> theory -> theory
   val local_path: theory -> theory
-  val conceal: theory -> theory
   val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
@@ -619,8 +619,6 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
-val conceal = map_naming Name_Space.conceal;
-
 val restore_naming = map_naming o K o naming_of;