# HG changeset patch
# User wenzelm
# Date 936629873 -7200
# Node ID c0f9b956a3e7fe68079c42367b9d50a34e39b2e9
# Parent  1f9eceb434dbe95725026a4faeba6048ac4d6a00
close_block: removed ProofContext.transfer_used_names;

diff -r 1f9eceb434db -r c0f9b956a3e7 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Sep 06 16:57:33 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Sep 06 16:57:53 1999 +0200
@@ -271,9 +271,7 @@
   |> open_block
   |> put_goal None;
 
-fun close_block (state as State (_, node :: nodes)) =
-      State (node, nodes)
-(* FIXME      |> map_context (ProofContext.transfer_used_names (context_of state)) *)
+fun close_block (state as State (_, node :: nodes)) = State (node, nodes)
   | close_block state = raise STATE ("Unbalanced block parentheses", state);