src/Pure/Isar/proof.ML
changeset 6731 57e761134c85
parent 6683 b7293047b0f4
child 6752 0545b77f864e
     1.1 --- a/src/Pure/Isar/proof.ML	Wed May 26 10:15:03 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed May 26 16:50:36 1999 +0200
     1.3 @@ -3,15 +3,6 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Proof states and methods.
     1.7 -
     1.8 -TODO:
     1.9 -  - assume: improve schematic Vars handling (!?);
    1.10 -  - warn_vars;
    1.11 -  - bind: check rhs (extra (T)Vars etc.) (How to handle these anyway?);
    1.12 -  - prep_result: avoid duplicate asms;
    1.13 -  - prep_result error: use error channel (!);
    1.14 -  - check_finished: trace results (!?);
    1.15 -  - next_block: fetch_facts (!?);
    1.16  *)
    1.17  
    1.18  signature PROOF =
    1.19 @@ -58,7 +49,8 @@
    1.20    val next_block: state -> state
    1.21    val end_block: state -> state
    1.22    val at_bottom: state -> bool
    1.23 -  val local_qed: (state -> state Seq.seq) -> bool -> state -> state Seq.seq
    1.24 +  val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit)
    1.25 +    -> state -> state Seq.seq
    1.26    val global_qed: (state -> state Seq.seq) -> bstring option
    1.27      -> theory attribute list option -> state -> theory * {kind: string, name: string, thm: thm}
    1.28  end;
    1.29 @@ -241,7 +233,7 @@
    1.30  fun assert_mode pred state =
    1.31    let val mode = get_mode state in
    1.32      if pred mode then state
    1.33 -    else raise STATE ("Illegal application of command in " ^ mode_name mode ^ " mode", state)
    1.34 +    else raise STATE ("Illegal application of proof command in " ^ mode_name mode ^ " mode", state)
    1.35    end;
    1.36  
    1.37  fun is_chain state = get_mode state = ForwardChain;
    1.38 @@ -367,7 +359,8 @@
    1.39        raw_thm RS Drule.rev_triv_goal
    1.40        |> implies_elim_hyps
    1.41        |> Drule.implies_intr_list asms
    1.42 -      |> varify_frees (ProofContext.fixed_names ctxt);
    1.43 +      |> varify_frees (ProofContext.fixed_names ctxt)
    1.44 +      |> Thm.varifyT;
    1.45  
    1.46      val {hyps, prop, sign, ...} = Thm.rep_thm thm;
    1.47      val tsig = Sign.tsig_of sign;
    1.48 @@ -608,7 +601,7 @@
    1.49  
    1.50  (* local_qed *)
    1.51  
    1.52 -fun finish_local state =
    1.53 +fun finish_local print_result state =
    1.54    let
    1.55      val ((kind, name, asms, t), (_, raw_thm)) = current_goal state;
    1.56      val result = prep_result state asms t raw_thm;
    1.57 @@ -618,16 +611,17 @@
    1.58        | Aux atts => (atts, Seq.single)
    1.59        | _ => raise STATE ("No local goal!", state));
    1.60    in
    1.61 +    print_result {kind = kind_name kind, name = name, thm = result};
    1.62      state
    1.63      |> close_block
    1.64      |> have_thmss name atts [Thm.no_attributes [result]]
    1.65      |> opt_solve
    1.66    end;
    1.67  
    1.68 -fun local_qed finalize int state =	(* FIXME handle int *)
    1.69 +fun local_qed finalize print_result state =
    1.70    state
    1.71    |> finish_proof false finalize
    1.72 -  |> (Seq.flat o Seq.map finish_local);
    1.73 +  |> (Seq.flat o Seq.map (finish_local print_result));
    1.74  
    1.75  
    1.76  (* global_qed *)