# HG changeset patch
# User wenzelm
# Date 1165683947 -3600
# Node ID 5acd4f35d26fee4832fa3056ae218b71a59931ba
# Parent  092b967da9b7f3cc27b9226ac38215518d38365f
init_context: reset naming;

diff -r 092b967da9b7 -r 5acd4f35d26f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Dec 09 18:05:46 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Dec 09 18:05:47 2006 +0100
@@ -154,8 +154,11 @@
 fun map_node f (Node {context, facts, mode, goal}) =
   make_node (f (context, facts, mode, goal));
 
+val init_context =
+  ProofContext.set_stmt true #> ProofContext.reset_naming;
+
 fun init ctxt =
-  State (Stack.init (make_node (ProofContext.set_stmt true ctxt, NONE, Forward, NONE)));
+  State (Stack.init (make_node (init_context 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);
@@ -772,7 +775,7 @@
       fn results => map_context after_ctxt #> after_local results);
   in
     goal_state
-    |> map_context (Variable.set_body true #> ProofContext.set_stmt true)
+    |> map_context (init_context #> Variable.set_body true)
     |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
     |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
     |> map_context (ProofContext.auto_bind_goal props)