# HG changeset patch # User wenzelm # Date 931112436 -7200 # Node ID 4bdc3600ddae2b4bbc8024cb391fbe333affbb0c # Parent 450b1f67f09954809266bb205d230a9dafe8cbd5 close_block: transfer_used_names; tuned; diff -r 450b1f67f099 -r 4bdc3600ddae src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sun Jul 04 20:19:28 1999 +0200 +++ b/src/Pure/Isar/proof.ML Sun Jul 04 20:20:36 1999 +0200 @@ -51,14 +51,14 @@ val show_i: string -> context attribute list -> term * term list -> state -> state val have: string -> context attribute list -> string * string list -> state -> state val have_i: string -> context attribute list -> term * term list -> state -> state - val begin_block: state -> state - val next_block: state -> state - val end_block: state -> state val at_bottom: state -> bool val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit) -> state -> state Seq.seq - val global_qed: (state -> state Seq.seq) -> bstring option - -> theory attribute list option -> state -> (theory * {kind: string, name: string, thm: thm}) Seq.seq + val global_qed: (state -> state Seq.seq) -> bstring option -> theory attribute list option + -> state -> (theory * {kind: string, name: string, thm: thm}) Seq.seq + val begin_block: state -> state + val end_block: state -> state + val next_block: state -> state end; signature PROOF_PRIVATE = @@ -254,7 +254,9 @@ |> open_block |> put_goal None; -fun close_block (State (_, node :: nodes)) = State (node, nodes) +fun close_block (state as State (_, node :: nodes)) = + State (node, nodes) + |> map_context (ProofContext.transfer_used_names (context_of state)) | close_block state = raise STATE ("Unbalanced block parentheses", state); @@ -542,28 +544,6 @@ -(** blocks **) - -(* begin_block *) - -fun begin_block state = - state - |> assert_forward - |> new_block - |> reset_facts - |> open_block; - - -(* next_block *) - -fun next_block state = - state - |> assert_forward - |> close_block - |> new_block; - - - (** conclusions **) (* current goal *) @@ -596,17 +576,6 @@ |> assert_current_goal true; -(* end_block *) - -fun end_block state = - state - |> assert_forward - |> close_block - |> assert_current_goal false - |> close_block - |> fetch_facts state; - - (* local_qed *) fun finish_local print_result state = @@ -659,4 +628,36 @@ |> Seq.map (finish_global alt_name alt_atts); + +(** blocks **) + +(* begin_block *) + +fun begin_block state = + state + |> assert_forward + |> new_block + |> open_block; + + +(* end_block *) + +fun end_block state = + state + |> assert_forward + |> close_block + |> assert_current_goal false + |> close_block + |> fetch_facts state; (* FIXME proper check / export (!?) *) + + +(* next_block *) + +fun next_block state = + state + |> assert_forward + |> close_block + |> new_block; + + end;