proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;

--- a/src/Pure/Proof/extraction.ML	Mon Jan 26 22:15:35 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Jan 27 00:29:37 2009 +0100
@@ -546,7 +546,7 @@
 
       | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
           let
-            val prf = force_proof body;
+            val prf = join_proof body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
             val T = etype_of thy' vs' [] prop;
@@ -570,7 +570,7 @@
                       (proof_combt
                          (PThm (serial (),
                           ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
-                            Lazy.value (make_proof_body corr_prf))), vfs_of corr_prop))
+                            Future.value (make_proof_body corr_prf))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop))
                   in
                     ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
@@ -636,7 +636,7 @@
 
       | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) =
           let
-            val prf = force_proof body;
+            val prf = join_proof body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
           in
@@ -681,7 +681,7 @@
                       (proof_combt
                         (PThm (serial (),
                          ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
-                           Lazy.value (make_proof_body corr_prf'))), vfs_of corr_prop))
+                           Future.value (make_proof_body corr_prf'))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop));
                   in
                     ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',

--- a/src/Pure/Proof/proof_syntax.ML	Mon Jan 26 22:15:35 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Jan 27 00:29:37 2009 +0100
@@ -228,7 +228,7 @@
     val prop = Thm.full_prop_of thm;
     val prf = Thm.proof_of thm;
     val prf' = (case strip_combt (fst (strip_combP prf)) of
-        (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then force_proof body else prf
+        (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else prf
       | _ => prf)
   in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
 

--- a/src/Pure/Proof/reconstruct.ML	Mon Jan 26 22:15:35 2009 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Tue Jan 27 00:29:37 2009 +0100
@@ -358,7 +358,7 @@
                     val _ = message ("Reconstructing proof of " ^ a);
                     val _ = message (Syntax.string_of_term_global thy prop);
                     val prf' = forall_intr_vfs_prf prop
-                      (reconstruct_proof thy prop (force_proof body));
+                      (reconstruct_proof thy prop (join_proof body));
                     val (maxidx', prfs', prf) = expand
                       (maxidx_proof prf' ~1) prfs prf'
                   in (maxidx' + maxidx + 1, inc (maxidx + 1) prf,

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jan 26 22:15:35 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jan 27 00:29:37 2009 +0100
@@ -256,7 +256,7 @@
   (case Thm.proof_body_of th of 
     PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
       if Thm.has_name_hint th andalso Thm.get_name_hint th = name
-      then add_proof_body (Lazy.force body)
+      then add_proof_body (Future.join body)
       else I
   | body => add_proof_body body);
 

--- a/src/Pure/Tools/xml_syntax.ML	Mon Jan 26 22:15:35 2009 +0100
+++ b/src/Pure/Tools/xml_syntax.ML	Tue Jan 27 00:29:37 2009 +0100
@@ -158,7 +158,7 @@
   | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
       (* FIXME? *)
       PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
-        Lazy.value (Proofterm.make_proof_body MinProof)))
+        Future.value (Proofterm.make_proof_body MinProof)))
   | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
       PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =

--- a/src/Pure/proofterm.ML	Mon Jan 26 22:15:35 2009 +0100
+++ b/src/Pure/proofterm.ML	Tue Jan 27 00:29:37 2009 +0100
@@ -21,10 +21,10 @@
    | PAxm of string * term * typ list option
    | Oracle of string * term * typ list option
    | Promise of serial * term * typ list
-   | PThm of serial * ((string * term * typ list option) * proof_body lazy)
+   | PThm of serial * ((string * term * typ list option) * proof_body future)
   and proof_body = PBody of
     {oracles: (string * term) OrdList.T,
-     thms: (serial * (string * term * proof_body lazy)) OrdList.T,
+     thms: (serial * (string * term * proof_body future)) OrdList.T,
      proof: proof}
 
   val %> : proof * term -> proof
@@ -35,10 +35,10 @@
   include BASIC_PROOFTERM
 
   type oracle = string * term
-  type pthm = serial * (string * term * proof_body lazy)
-  val force_body: proof_body lazy ->
+  type pthm = serial * (string * term * proof_body future)
+  val join_body: proof_body future ->
     {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
-  val force_proof: proof_body lazy -> proof
+  val join_proof: proof_body future -> proof
   val proof_of: proof_body -> proof
   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
@@ -142,17 +142,17 @@
  | PAxm of string * term * typ list option
  | Oracle of string * term * typ list option
  | Promise of serial * term * typ list
- | PThm of serial * ((string * term * typ list option) * proof_body lazy)
+ | PThm of serial * ((string * term * typ list option) * proof_body future)
 and proof_body = PBody of
   {oracles: (string * term) OrdList.T,
-   thms: (serial * (string * term * proof_body lazy)) OrdList.T,
+   thms: (serial * (string * term * proof_body future)) OrdList.T,
    proof: proof};
 
 type oracle = string * term;
-type pthm = serial * (string * term * proof_body lazy);
+type pthm = serial * (string * term * proof_body future);
 
-val force_body = Lazy.force #> (fn PBody args => args);
-val force_proof = #proof o force_body;
+val join_body = Future.join #> (fn PBody args => args);
+val join_proof = #proof o join_body;
 
 fun proof_of (PBody {proof, ...}) = proof;
 
@@ -165,7 +165,7 @@
       if Inttab.defined seen i then (x, seen)
       else
         let
-          val body' = Lazy.force body;
+          val body' = Future.join body;
           val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
         in (f (name, prop, body') x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
@@ -180,7 +180,7 @@
           if Inttab.defined seen i then (x, seen)
           else
             let val (x', seen') =
-              (if all then app (force_proof body) else I) (x, Inttab.update (i, ()) seen)
+              (if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen)
             in (f prf x', seen') end)
       | app prf = (fn (x, seen) => (f prf x, seen));
   in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end;
@@ -233,7 +233,7 @@
 
 fun strip_thm (body as PBody {proof, ...}) =
   (case strip_combt (fst (strip_combP proof)) of
-    (PThm (_, (_, body')), _) => Lazy.force body'
+    (PThm (_, (_, body')), _) => Future.join body'
   | _ => body);
 
 val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
@@ -1245,7 +1245,7 @@
       else MinProof;
 
     fun new_prf () = (serial (), name, prop,
-      Lazy.lazy (fn () => fulfill_proof thy (Lazy.force promises)
+      Future.fork_pri ~2 (fn () => fulfill_proof thy (Lazy.force promises)
         (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
 
     val (i, name, prop, body') =