src/Pure/Isar/proof.ML
changeset 28446 a01de3b3fa2e
parent 28443 de653f1ad78b
child 28450 504c4edead13
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Oct 01 12:00:05 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Oct 01 12:18:18 2008 +0200
     1.3 @@ -114,8 +114,8 @@
     1.4      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
     1.5    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     1.6      ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
     1.7 -  val can_promise: state -> bool
     1.8 -  val promise_proof: (state -> context) -> state -> context
     1.9 +  val can_defer: state -> bool
    1.10 +  val future_proof: (state -> context) -> state -> context
    1.11  end;
    1.12  
    1.13  structure Proof: PROOF =
    1.14 @@ -976,22 +976,22 @@
    1.15  end;
    1.16  
    1.17  
    1.18 -(* promise global proofs *)
    1.19 +(* defer global proofs *)
    1.20  
    1.21  fun is_initial state =
    1.22    (case try find_goal state of
    1.23      NONE => false
    1.24    | SOME (_, (_, {statement = (_, _, prop), goal, ...})) => Thm.eq_thm_prop (Goal.init prop, goal));
    1.25  
    1.26 -fun can_promise state =
    1.27 +fun can_defer state =
    1.28    can (assert_bottom true) state andalso
    1.29    can assert_backward state andalso
    1.30    is_initial state andalso
    1.31    not (schematic_goal state);
    1.32  
    1.33 -fun promise_proof make_proof state =
    1.34 +fun future_proof make_proof state =
    1.35    let
    1.36 -    val _ = can_promise state orelse error "Cannot promise proof";
    1.37 +    val _ = can_defer state orelse error "Cannot defer proof";
    1.38  
    1.39      val (goal_ctxt, (_, goal)) = find_goal state;
    1.40      val {statement as (kind, propss, cprop), messages, using, goal, before_qed, after_qed} = goal;
    1.41 @@ -1005,7 +1005,7 @@
    1.42        |> map_goal I (K (statement', messages, using, goal, before_qed, (#1 after_qed, after_qed')))
    1.43        |> make_proof
    1.44        |> (fn result_ctxt => ProofContext.get_fact_single result_ctxt (Facts.named this_name));
    1.45 -    val finished_goal = Goal.protect (Goal.promise_result goal_ctxt make_result prop);
    1.46 +    val finished_goal = Goal.protect (Goal.future_result goal_ctxt make_result prop);
    1.47    in
    1.48      state
    1.49      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))