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)));