close_block: removed ProofContext.transfer_used_names;
authorwenzelm
Mon Sep 06 16:57:53 1999 +0200 (1999-09-06)
changeset 7487c0f9b956a3e7
parent 7486 1f9eceb434db
child 7488 c49d17fac066
close_block: removed ProofContext.transfer_used_names;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Sep 06 16:57:33 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Sep 06 16:57:53 1999 +0200
     1.3 @@ -271,9 +271,7 @@
     1.4    |> open_block
     1.5    |> put_goal None;
     1.6  
     1.7 -fun close_block (state as State (_, node :: nodes)) =
     1.8 -      State (node, nodes)
     1.9 -(* FIXME      |> map_context (ProofContext.transfer_used_names (context_of state)) *)
    1.10 +fun close_block (state as State (_, node :: nodes)) = State (node, nodes)
    1.11    | close_block state = raise STATE ("Unbalanced block parentheses", state);
    1.12  
    1.13