1.1 --- a/src/Pure/goal.ML	Wed Oct 01 12:00:05 2008 +0200
     1.2 +++ b/src/Pure/goal.ML	Wed Oct 01 12:18:18 2008 +0200
     1.3 @@ -20,11 +20,11 @@
     1.4    val conclude: thm -> thm
     1.5    val finish: thm -> thm
     1.6    val norm_result: thm -> thm
     1.7 -  val promise_result: Proof.context -> (unit -> thm) -> term -> thm
     1.8 +  val future_result: Proof.context -> (unit -> thm) -> term -> thm
     1.9    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.10    val prove_multi: Proof.context -> string list -> term list -> term list ->
    1.11      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    1.12 -  val prove_promise: Proof.context -> string list -> term list -> term ->
    1.13 +  val prove_future: Proof.context -> string list -> term list -> term ->
    1.14      ({prems: thm list, context: Proof.context} -> tactic) -> thm
    1.15    val prove: Proof.context -> string list -> term list -> term ->
    1.16      ({prems: thm list, context: Proof.context} -> tactic) -> thm
    1.17 @@ -96,9 +96,9 @@
    1.18    #> Drule.zero_var_indexes;
    1.19  
    1.20  
    1.21 -(* promise *)
    1.22 +(* future_result *)
    1.23  
    1.24 -fun promise_result ctxt result prop =
    1.25 +fun future_result ctxt result prop =
    1.26    let
    1.27      val thy = ProofContext.theory_of ctxt;
    1.28      val _ = Context.reject_draft thy;
    1.29 @@ -122,7 +122,7 @@
    1.30        Drule.implies_intr_list assms o
    1.31        Thm.adjust_maxidx_thm ~1 o result;
    1.32      val local_result =
    1.33 -      Thm.promise global_result (cert global_prop)
    1.34 +      Thm.future global_result (cert global_prop)
    1.35        |> Thm.instantiate (instT, [])
    1.36        |> Drule.forall_elim_list fixes
    1.37        |> fold (Thm.elim_implies o Thm.assume) assms;
    1.38 @@ -176,7 +176,7 @@
    1.39            end);
    1.40      val res =
    1.41        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
    1.42 -      else promise_result ctxt' result (Thm.term_of stmt);
    1.43 +      else future_result ctxt' result (Thm.term_of stmt);
    1.44    in
    1.45      Conjunction.elim_balanced (length props) res
    1.46      |> map (Assumption.export false ctxt' ctxt)
    1.47 @@ -186,7 +186,7 @@
    1.48  
    1.49  val prove_multi = prove_common true;
    1.50  
    1.51 -fun prove_promise ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
    1.52 +fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
    1.53  fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
    1.54  
    1.55  fun prove_global thy xs asms prop tac =