# HG changeset patch
# User wenzelm
# Date 1222597424 -7200
# Node ID 777bdc429ea382d6a49eb13c1067a16f0de9cca5
# Parent  0789bbedfc62409854b135b50eb4068a6e1caa54
promise_result: enforce strictly sequential dependencies, via serial numbers;

diff -r 0789bbedfc62 -r 777bdc429ea3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Sep 28 09:25:24 2008 +0200
+++ b/src/Pure/thm.ML	Sun Sep 28 12:23:44 2008 +0200
@@ -1622,18 +1622,19 @@
 
 (* promise *)
 
-fun promise_result orig_thy orig_shyps orig_prop raw_thm =
+fun promise_result i orig_thy orig_shyps orig_prop raw_thm =
   let
     val _ = Theory.check_thy orig_thy;
     val thm = strip_shyps (transfer orig_thy raw_thm);
     val _ = Theory.check_thy orig_thy;
     fun err msg = raise THM ("promise_result: " ^ msg, 0, [thm]);
 
-    val Thm (_, {shyps, hyps, tpairs, prop, ...}) = thm;
+    val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
     val _ = prop aconv orig_prop orelse err "bad prop";
     val _ = null tpairs orelse err "bad tpairs";
     val _ = null hyps orelse err "bad hyps";
     val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
+    val _ = forall (fn (j, _) => j < i) promises orelse err "bad dependencies";
   in thm end;
 
 fun promise make_result ct =
@@ -1642,9 +1643,9 @@
     val thy = Context.reject_draft (Theory.deref thy_ref);
     val _ = T <> propT andalso raise CTERM ("promise: prop expected", [ct]);
 
-    val future = Future.fork_irrelevant (promise_result thy sorts prop o make_result);
+    val i = serial ();
+    val future = Future.fork_irrelevant (promise_result i thy sorts prop o make_result);
     val _ = add_future thy future;
-    val i = serial ();
   in
     Thm (make_deriv false [(i, future)] (Pt.promise_proof i prop),
      {thy_ref = thy_ref,