1.1 --- a/src/Pure/thm.ML	Wed Oct 01 12:00:05 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed Oct 01 12:18:18 2008 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4    val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
     1.5    val freezeT: thm -> thm
     1.6    val join_futures: theory -> unit
     1.7 -  val promise: (unit -> thm) -> cterm -> thm
     1.8 +  val future: (unit -> thm) -> cterm -> thm
     1.9    val proof_of: thm -> Proofterm.proof
    1.10    val extern_oracles: theory -> xstring list
    1.11    val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
    1.12 @@ -1625,14 +1625,14 @@
    1.13    in while not (joined ()) do () end;
    1.14  
    1.15  
    1.16 -(* promise *)
    1.17 +(* future rule *)
    1.18  
    1.19 -fun promise_result i orig_thy orig_shyps orig_prop raw_thm =
    1.20 +fun future_result i orig_thy orig_shyps orig_prop raw_thm =
    1.21    let
    1.22      val _ = Theory.check_thy orig_thy;
    1.23      val thm = strip_shyps (transfer orig_thy raw_thm);
    1.24      val _ = Theory.check_thy orig_thy;
    1.25 -    fun err msg = raise THM ("promise_result: " ^ msg, 0, [thm]);
    1.26 +    fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
    1.27  
    1.28      val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
    1.29      val _ = prop aconv orig_prop orelse err "bad prop";
    1.30 @@ -1642,14 +1642,14 @@
    1.31      val _ = forall (fn (j, _) => j < i) promises orelse err "bad dependencies";
    1.32    in thm end;
    1.33  
    1.34 -fun promise make_result ct =
    1.35 +fun future make_result ct =
    1.36    let
    1.37      val {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = rep_cterm ct;
    1.38      val thy = Context.reject_draft (Theory.deref thy_ref);
    1.39 -    val _ = T <> propT andalso raise CTERM ("promise: prop expected", [ct]);
    1.40 +    val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
    1.41  
    1.42      val i = serial ();
    1.43 -    val future = Future.fork_background (promise_result i thy sorts prop o make_result);
    1.44 +    val future = Future.fork_background (future_result i thy sorts prop o make_result);
    1.45      val _ = add_future thy future;
    1.46    in
    1.47      Thm (make_deriv false [(i, future)] (Pt.promise_proof i prop),
    1.48 @@ -1663,9 +1663,9 @@
    1.49    end;
    1.50  
    1.51  
    1.52 -(* fulfill *)
    1.53 +(* join_deriv *)
    1.54  
    1.55 -fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
    1.56 +fun join_deriv (thm as Thm (Deriv {oracle, proof, promises}, args)) =
    1.57    let
    1.58      val _ = Exn.release_all (Future.join_results (rev (map #2 promises)));
    1.59      val results = map (apsnd Future.join) promises;
    1.60 @@ -1674,7 +1674,7 @@
    1.61      val ora = oracle orelse exists (oracle_of o #2) results;
    1.62    in Thm (make_deriv ora [] (Pt.fulfill proofs proof), args) end;
    1.63  
    1.64 -val proof_of = fulfill #> (fn Thm (Deriv {proof, ...}, _) => proof);
    1.65 +val proof_of = join_deriv #> (fn Thm (Deriv {proof, ...}, _) => proof);
    1.66  
    1.67  
    1.68