init: enter inner statement mode, which prevents local notes from being named internally;

--- a/src/Pure/Isar/proof.ML	Wed Nov 22 15:58:15 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Nov 22 15:58:59 2006 +0100
@@ -154,7 +154,8 @@
 fun map_node f (Node {context, facts, mode, goal}) =
   make_node (f (context, facts, mode, goal));
 
-fun init ctxt = State (Stack.init (make_node (ctxt, NONE, Forward, NONE)));
+fun init ctxt =
+  State (Stack.init (make_node (ProofContext.set_stmt true ctxt, NONE, Forward, NONE)));
 
 fun current (State st) = Stack.top st |> (fn Node node => node);
 fun map_current f (State st) = State (Stack.map_top (map_node f) st);