author | wenzelm |
Mon, 06 Sep 1999 16:57:53 +0200 | |
changeset 7487 | c0f9b956a3e7 |
parent 7486 | 1f9eceb434db |
child 7488 | c49d17fac066 |
--- 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);