close_block: transfer_used_names;
authorwenzelm
Sun Jul 04 20:20:36 1999 +0200 (1999-07-04)
changeset 68964bdc3600ddae
parent 6895 450b1f67f099
child 6897 cc6e50f36da8
close_block: transfer_used_names;
tuned;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Jul 04 20:19:28 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Jul 04 20:20:36 1999 +0200
     1.3 @@ -51,14 +51,14 @@
     1.4    val show_i: string -> context attribute list -> term * term list -> state -> state
     1.5    val have: string -> context attribute list -> string * string list -> state -> state
     1.6    val have_i: string -> context attribute list -> term * term list -> state -> state
     1.7 -  val begin_block: state -> state
     1.8 -  val next_block: state -> state
     1.9 -  val end_block: state -> state
    1.10    val at_bottom: state -> bool
    1.11    val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit)
    1.12      -> state -> state Seq.seq
    1.13 -  val global_qed: (state -> state Seq.seq) -> bstring option
    1.14 -    -> theory attribute list option -> state -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
    1.15 +  val global_qed: (state -> state Seq.seq) -> bstring option -> theory attribute list option
    1.16 +    -> state -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
    1.17 +  val begin_block: state -> state
    1.18 +  val end_block: state -> state
    1.19 +  val next_block: state -> state
    1.20  end;
    1.21  
    1.22  signature PROOF_PRIVATE =
    1.23 @@ -254,7 +254,9 @@
    1.24    |> open_block
    1.25    |> put_goal None;
    1.26  
    1.27 -fun close_block (State (_, node :: nodes)) = State (node, nodes)
    1.28 +fun close_block (state as State (_, node :: nodes)) =
    1.29 +      State (node, nodes)
    1.30 +      |> map_context (ProofContext.transfer_used_names (context_of state))
    1.31    | close_block state = raise STATE ("Unbalanced block parentheses", state);
    1.32  
    1.33  
    1.34 @@ -542,28 +544,6 @@
    1.35  
    1.36  
    1.37  
    1.38 -(** blocks **)
    1.39 -
    1.40 -(* begin_block *)
    1.41 -
    1.42 -fun begin_block state =
    1.43 -  state
    1.44 -  |> assert_forward
    1.45 -  |> new_block
    1.46 -  |> reset_facts
    1.47 -  |> open_block;
    1.48 -
    1.49 -
    1.50 -(* next_block *)
    1.51 -
    1.52 -fun next_block state =
    1.53 -  state
    1.54 -  |> assert_forward
    1.55 -  |> close_block
    1.56 -  |> new_block;
    1.57 -
    1.58 -
    1.59 -
    1.60  (** conclusions **)
    1.61  
    1.62  (* current goal *)
    1.63 @@ -596,17 +576,6 @@
    1.64    |> assert_current_goal true;
    1.65  
    1.66  
    1.67 -(* end_block *)
    1.68 -
    1.69 -fun end_block state =
    1.70 -  state
    1.71 -  |> assert_forward
    1.72 -  |> close_block
    1.73 -  |> assert_current_goal false
    1.74 -  |> close_block
    1.75 -  |> fetch_facts state;
    1.76 -
    1.77 -
    1.78  (* local_qed *)
    1.79  
    1.80  fun finish_local print_result state =
    1.81 @@ -659,4 +628,36 @@
    1.82    |> Seq.map (finish_global alt_name alt_atts);
    1.83  
    1.84  
    1.85 +
    1.86 +(** blocks **)
    1.87 +
    1.88 +(* begin_block *)
    1.89 +
    1.90 +fun begin_block state =
    1.91 +  state
    1.92 +  |> assert_forward
    1.93 +  |> new_block
    1.94 +  |> open_block;
    1.95 +
    1.96 +
    1.97 +(* end_block *)
    1.98 +
    1.99 +fun end_block state =
   1.100 +  state
   1.101 +  |> assert_forward
   1.102 +  |> close_block
   1.103 +  |> assert_current_goal false
   1.104 +  |> close_block
   1.105 +  |> fetch_facts state;          (* FIXME proper check / export (!?) *)
   1.106 +
   1.107 +
   1.108 +(* next_block *)
   1.109 +
   1.110 +fun next_block state =
   1.111 +  state
   1.112 +  |> assert_forward
   1.113 +  |> close_block
   1.114 +  |> new_block;
   1.115 +
   1.116 +
   1.117  end;