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

     2.1 --- a/src/Pure/Isar/proof_context.ML	Sun Oct 25 19:14:46 2009 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Oct 25 19:17:42 2009 +0100
     2.3 @@ -21,7 +21,10 @@
     2.4    val restore_mode: Proof.context -> Proof.context -> Proof.context
     2.5    val abbrev_mode: Proof.context -> bool
     2.6    val set_stmt: bool -> Proof.context -> Proof.context
     2.7 +  val local_naming: Name_Space.naming
     2.8 +  val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
     2.9    val naming_of: Proof.context -> Name_Space.naming
    2.10 +  val restore_naming: Proof.context -> Proof.context -> Proof.context
    2.11    val full_name: Proof.context -> binding -> string
    2.12    val consts_of: Proof.context -> Consts.T
    2.13    val const_syntax_name: Proof.context -> string -> string
    2.14 @@ -92,11 +95,6 @@
    2.15    val get_fact_single: Proof.context -> Facts.ref -> thm
    2.16    val get_thms: Proof.context -> xstring -> thm list
    2.17    val get_thm: Proof.context -> xstring -> thm
    2.18 -  val add_path: string -> Proof.context -> Proof.context
    2.19 -  val mandatory_path: string -> Proof.context -> Proof.context
    2.20 -  val conceal: Proof.context -> Proof.context
    2.21 -  val restore_naming: Proof.context -> Proof.context -> Proof.context
    2.22 -  val reset_naming: Proof.context -> Proof.context
    2.23    val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
    2.24      Proof.context -> (string * thm list) list * Proof.context
    2.25    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
    2.26 @@ -232,6 +230,7 @@
    2.27    map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
    2.28  
    2.29  val naming_of = #naming o rep_context;
    2.30 +val restore_naming = map_naming o K o naming_of
    2.31  val full_name = Name_Space.full_name o naming_of;
    2.32  
    2.33  val syntax_of = #syntax o rep_context;
    2.34 @@ -923,15 +922,6 @@
    2.35  end;
    2.36  
    2.37  
    2.38 -(* name space operations *)
    2.39 -
    2.40 -val add_path = map_naming o Name_Space.add_path;
    2.41 -val mandatory_path = map_naming o Name_Space.mandatory_path;
    2.42 -val conceal = map_naming Name_Space.conceal;
    2.43 -val restore_naming = map_naming o K o naming_of;
    2.44 -val reset_naming = map_naming (K local_naming);
    2.45 -
    2.46 -
    2.47  (* facts *)
    2.48  
    2.49  local

     3.1 --- a/src/Pure/sign.ML	Sun Oct 25 19:14:46 2009 +0100
     3.2 +++ b/src/Pure/sign.ML	Sun Oct 25 19:17:42 2009 +0100
     3.3 @@ -12,6 +12,7 @@
     3.4      syn: Syntax.syntax,
     3.5      tsig: Type.tsig,
     3.6      consts: Consts.T}
     3.7 +  val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
     3.8    val naming_of: theory -> Name_Space.naming
     3.9    val full_name: theory -> binding -> string
    3.10    val full_name_path: theory -> string -> binding -> string
    3.11 @@ -125,7 +126,6 @@
    3.12    val parent_path: theory -> theory
    3.13    val mandatory_path: string -> theory -> theory
    3.14    val local_path: theory -> theory
    3.15 -  val conceal: theory -> theory
    3.16    val restore_naming: theory -> theory -> theory
    3.17    val hide_class: bool -> string -> theory -> theory
    3.18    val hide_type: bool -> string -> theory -> theory
    3.19 @@ -619,8 +619,6 @@
    3.20  
    3.21  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    3.22  
    3.23 -val conceal = map_naming Name_Space.conceal;
    3.24 -
    3.25  val restore_naming = map_naming o K o naming_of;
    3.26  
    3.27