# HG changeset patch
# User haftmann
# Date 1228460714 -3600
# Node ID c4ae153d78ab42e120db136a9f38fe08ccfa3219
# Parent  3d8f01383117ec532cb21d4322ec745bc1ef54bb# Parent  694227dd3e8ca7a5e73030235f9df1c09c32be73
merged

diff -r 694227dd3e8c -r c4ae153d78ab Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Fri Dec 05 08:04:53 2008 +0100
+++ b/Admin/isatest/isatest-makeall	Fri Dec 05 08:05:14 2008 +0100
@@ -133,6 +133,11 @@
 
     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
 
+    if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then
+        echo "--- cleaning up old $ISABELLE_HOME_USER"
+        rm -rf $ISABELLE_HOME_USER
+    fi
+
     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
     (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1)
 
diff -r 694227dd3e8c -r c4ae153d78ab Admin/isatest/settings/sun-poly
--- a/Admin/isatest/settings/sun-poly	Fri Dec 05 08:04:53 2008 +0100
+++ b/Admin/isatest/settings/sun-poly	Fri Dec 05 08:05:14 2008 +0100
@@ -6,7 +6,7 @@
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 1500"
 
-ISABELLE_HOME_USER=~/isabelle-sun-poly
+ISABELLE_HOME_USER=/tmp/isabelle-sun-poly
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
diff -r 694227dd3e8c -r c4ae153d78ab src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Fri Dec 05 08:05:14 2008 +0100
@@ -169,16 +169,20 @@
   proof qed (auto simp add: ring_simps power_Suc)
 
 lemmas nat_arith =
-  add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
+  add_nat_number_of
+  diff_nat_number_of
+  mult_nat_number_of
+  eq_nat_number_of
+  less_nat_number_of
 
 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
   by (simp add: numeral_1_eq_1)
+
 lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
   if_True add_0 add_Suc add_number_of_left mult_number_of_left
   numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
-  numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1
-  iszero_number_of_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min
-  iszero_number_of_Pls iszero_0 not_iszero_Numeral1
+  numeral_0_eq_0[symmetric] numerals[symmetric]
+  iszero_simps not_iszero_Numeral1
 
 lemmas semiring_norm = comp_arith
 
@@ -458,7 +462,6 @@
 declare zmod_eq_dvd_iff[algebra]
 declare nat_mod_eq_iff[algebra]
 
-
 subsection{* Groebner Bases for fields *}
 
 interpretation class_fieldgb:
@@ -607,14 +610,6 @@
              @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
              name = "ord_frac_simproc", proc = proc3, identifier = []}
 
-val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
-               "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
-
-val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
-                 "add_Suc", "add_number_of_left", "mult_number_of_left",
-                 "Suc_eq_add_numeral_1"])@
-                 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
-                 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
            @{thm "divide_Numeral1"},
            @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
@@ -630,7 +625,7 @@
 in
 val comp_conv = (Simplifier.rewrite
 (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
-              addsimps ths addsimps comp_arith addsimps simp_thms
+              addsimps ths addsimps simp_thms
               addsimprocs field_cancel_numeral_factors
                addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
                             ord_frac_simproc]
diff -r 694227dd3e8c -r c4ae153d78ab src/HOL/Import/lazy_seq.ML
--- a/src/HOL/Import/lazy_seq.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/HOL/Import/lazy_seq.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -80,7 +80,7 @@
 structure LazySeq :> LAZY_SEQ =
 struct
 
-datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T
+datatype 'a seq = Seq of ('a * 'a seq) option lazy
 
 exception Empty
 
diff -r 694227dd3e8c -r c4ae153d78ab src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/HOL/Int.thy	Fri Dec 05 08:05:14 2008 +0100
@@ -855,7 +855,7 @@
     add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
 qed
 
-lemma neg_simps:
+lemma bin_less_0_simps:
   "Pls < 0 \<longleftrightarrow> False"
   "Min < 0 \<longleftrightarrow> True"
   "Bit0 w < 0 \<longleftrightarrow> w < 0"
@@ -908,7 +908,7 @@
     less_bin_lemma [of "Bit1 k"]
     less_bin_lemma [of "pred Pls"]
     less_bin_lemma [of "pred k"]
-  by (simp_all add: neg_simps succ_pred)
+  by (simp_all add: bin_less_0_simps succ_pred)
 
 text {* Less-than-or-equal *}
 
@@ -1187,6 +1187,12 @@
     by (auto simp add: iszero_def number_of_eq numeral_simps)
 qed
 
+lemmas iszero_simps =
+  iszero_0 not_iszero_1
+  iszero_number_of_Pls nonzero_number_of_Min
+  iszero_number_of_Bit0 iszero_number_of_Bit1
+(* iszero_number_of_Pls would never normally be used
+   because its lhs simplifies to "iszero 0" *)
 
 subsubsection {* The Less-Than Relation *}
 
@@ -1248,6 +1254,10 @@
   by (simp add: neg_def number_of_eq numeral_simps)
 qed
 
+lemmas neg_simps =
+  not_neg_0 not_neg_1
+  not_neg_number_of_Pls neg_number_of_Min
+  neg_number_of_Bit0 neg_number_of_Bit1
 
 text {* Less-Than or Equals *}
 
@@ -1307,15 +1317,15 @@
   "(number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y \<longleftrightarrow> x \<le> y"
   unfolding number_of_eq by (rule of_int_le_iff)
 
+lemma eq_number_of [simp]:
+  "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
+  unfolding number_of_eq by (rule of_int_eq_iff)
+
 lemmas rel_simps [simp] = 
   less_number_of less_bin_simps
   le_number_of le_bin_simps
-  eq_number_of_eq iszero_0 nonzero_number_of_Min
-  iszero_number_of_Bit0 iszero_number_of_Bit1
-  not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
-  neg_number_of_Min neg_number_of_Bit0 neg_number_of_Bit1
-(* iszero_number_of_Pls would never be used
-   because its lhs simplifies to "iszero 0" *)
+  eq_number_of_eq eq_bin_simps
+  iszero_simps neg_simps
 
 
 subsubsection {* Simplification of arithmetic when nested to the right. *}
@@ -1576,17 +1586,17 @@
 
 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
 lemmas less_special =
-  binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
-  binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
-  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
-  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
+  binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
+  binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
+  binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
+  binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
 
 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
 lemmas le_special =
-    binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
-    binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
-    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
-    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
+    binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
+    binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
+    binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
+    binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
 
 lemmas arith_special[simp] = 
        add_special diff_special eq_special less_special le_special
diff -r 694227dd3e8c -r c4ae153d78ab src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Dec 05 08:05:14 2008 +0100
@@ -349,7 +349,7 @@
 
 lemma nat_code' [code]:
   "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
-  by auto
+  unfolding nat_number_of_def number_of_is_id neg_def by simp
 
 lemma of_nat_int [code unfold]:
   "of_nat = int" by (simp add: int_def)
diff -r 694227dd3e8c -r c4ae153d78ab src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/HOL/Library/Float.thy	Fri Dec 05 08:05:14 2008 +0100
@@ -499,7 +499,7 @@
 
 lemma int_eq_number_of_eq:
   "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
-  by simp
+  by (rule eq_number_of_eq)
 
 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
   by (simp only: iszero_number_of_Pls)
@@ -514,7 +514,7 @@
   by simp
 
 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
-  unfolding neg_def number_of_is_id by simp
+  by (rule less_number_of_eq_neg)
 
 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
   by simp
diff -r 694227dd3e8c -r c4ae153d78ab src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/HOL/NatBin.thy	Fri Dec 05 08:05:14 2008 +0100
@@ -111,8 +111,8 @@
      "int (number_of v) =  
          (if neg (number_of v :: int) then 0  
           else (number_of v :: int))"
-by (simp del: nat_number_of
-	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by simp
 
 
 subsubsection{*Successor *}
@@ -124,10 +124,9 @@
 
 lemma Suc_nat_number_of_add:
      "Suc (number_of v + n) =  
-        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)" 
-by (simp del: nat_number_of 
-         add: nat_number_of_def neg_nat
-              Suc_nat_eq_nat_zadd1 number_of_succ) 
+        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
+  unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
+  by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
 
 lemma Suc_nat_number_of [simp]:
      "Suc (number_of v) =  
@@ -145,7 +144,8 @@
          (if neg (number_of v :: int) then number_of v'  
           else if neg (number_of v' :: int) then number_of v  
           else number_of (v + v'))"
-by (simp add: neg_nat nat_number_of_def nat_add_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_add_distrib)
 
 
 subsubsection{*Subtraction *}
@@ -172,7 +172,8 @@
 lemma mult_nat_number_of [simp]:
      "(number_of v :: nat) * number_of v' =  
        (if neg (number_of v :: int) then 0 else number_of (v * v'))"
-by (simp add: neg_nat nat_number_of_def nat_mult_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_mult_distrib)
 
 
 subsubsection{*Quotient *}
@@ -181,7 +182,8 @@
      "(number_of v :: nat)  div  number_of v' =  
           (if neg (number_of v :: int) then 0  
            else nat (number_of v div number_of v'))"
-by (simp add: neg_nat nat_number_of_def nat_div_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_div_distrib)
 
 lemma one_div_nat_number_of [simp]:
      "Suc 0 div number_of v' = nat (1 div number_of v')" 
@@ -195,7 +197,8 @@
         (if neg (number_of v :: int) then 0  
          else if neg (number_of v' :: int) then number_of v  
          else nat (number_of v mod number_of v'))"
-by (simp add: neg_nat nat_number_of_def nat_mod_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_mod_distrib)
 
 lemma one_mod_nat_number_of [simp]:
      "Suc 0 mod number_of v' =  
@@ -246,15 +249,11 @@
 (*"neg" is used in rewrite rules for binary comparisons*)
 lemma eq_nat_number_of [simp]:
      "((number_of v :: nat) = number_of v') =  
-      (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))  
-       else if neg (number_of v' :: int) then iszero (number_of v :: int)  
-       else iszero (number_of (v + uminus v') :: int))"
-apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
-                  eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
-            split add: split_if cong add: imp_cong)
-apply (simp only: nat_eq_iff nat_eq_iff2)
-apply (simp add: not_neg_eq_ge_0 [symmetric])
-done
+      (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
+       else if neg (number_of v' :: int) then (number_of v :: int) = 0
+       else v = v')"
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by auto
 
 
 subsubsection{*Less-than (<) *}
@@ -441,13 +440,11 @@
 text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
 
 lemma eq_number_of_0 [simp]:
-     "(number_of v = (0::nat)) =  
-      (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
+  "number_of v = (0::nat) \<longleftrightarrow> number_of v \<le> (0::int)"  
+  unfolding nat_number_of_def number_of_is_id by auto
 
 lemma eq_0_number_of [simp]:
-     "((0::nat) = number_of v) =  
-      (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
+  "(0::nat) = number_of v \<longleftrightarrow> number_of v \<le> (0::int)"  
 by (rule trans [OF eq_sym_conv eq_number_of_0])
 
 lemma less_0_number_of [simp]:
@@ -456,7 +453,7 @@
 
 
 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
+by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
 
 
 
@@ -643,26 +640,15 @@
 
 lemma nat_number_of_Bit0:
     "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
-  apply (simp only: nat_number_of_def Let_def)
-  apply (cases "neg (number_of w :: int)")
-   apply (simp add: neg_nat neg_number_of_Bit0)
-  apply (rule int_int_eq [THEN iffD1])
-  apply (simp only: not_neg_nat neg_number_of_Bit0 int_Suc zadd_int [symmetric] simp_thms)
-  apply (simp only: number_of_Bit0 zadd_assoc)
-  apply simp
-  done
+  unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
+  by auto
 
 lemma nat_number_of_Bit1:
   "number_of (Int.Bit1 w) =
     (if neg (number_of w :: int) then 0
      else let n = number_of w in Suc (n + n))"
-  apply (simp only: nat_number_of_def Let_def split: split_if)
-  apply (intro conjI impI)
-   apply (simp add: neg_nat neg_number_of_Bit1)
-  apply (rule int_int_eq [THEN iffD1])
-  apply (simp only: not_neg_nat neg_number_of_Bit1 int_Suc zadd_int [symmetric] simp_thms)
-  apply (simp only: number_of_Bit1 zadd_assoc)
-  done
+  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
+  by auto
 
 lemmas nat_number =
   nat_number_of_Pls nat_number_of_Min
@@ -708,7 +694,8 @@
          (if neg (number_of v :: int) then number_of v' + k  
           else if neg (number_of v' :: int) then number_of v + k  
           else number_of (v + v') + k)"
-by simp
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by auto
 
 lemma nat_number_of_mult_left:
      "number_of v * (number_of v' * (k::nat)) =  
diff -r 694227dd3e8c -r c4ae153d78ab src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/HOL/Presburger.thy	Fri Dec 05 08:05:14 2008 +0100
@@ -411,7 +411,7 @@
   by (simp cong: conj_cong)
 lemma int_eq_number_of_eq:
   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
-  by simp
+  by (rule eq_number_of_eq)
 
 lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
 unfolding dvd_eq_mod_eq_0[symmetric] ..
diff -r 694227dd3e8c -r c4ae153d78ab src/HOL/Tools/ComputeNumeral.thy
--- a/src/HOL/Tools/ComputeNumeral.thy	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/HOL/Tools/ComputeNumeral.thy	Fri Dec 05 08:05:14 2008 +0100
@@ -116,7 +116,7 @@
 lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)"
   apply (simp add: nat_norm_number_of_def)
   unfolding lezero_def iszero_def neg_def
-  apply (simp add: number_of_is_id)
+  apply (simp add: numeral_simps)
   done
 
 (* Normalization of nat literals *)
@@ -143,6 +143,7 @@
   apply (auto simp add: number_of_is_id neg_def iszero_def)
   apply (case_tac "x > 0")
   apply auto
+  apply (rule order_less_imp_le)
   apply (simp add: mult_strict_left_mono[where a=y and b=0 and c=x, simplified])
   done
 
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -30,21 +30,23 @@
   val enabled: unit -> bool
   type task = TaskQueue.task
   type group = TaskQueue.group
-  val thread_data: unit -> (string * task * group) option
-  type 'a T
-  val task_of: 'a T -> task
-  val group_of: 'a T -> group
-  val peek: 'a T -> 'a Exn.result option
-  val is_finished: 'a T -> bool
-  val future: group option -> task list -> bool -> (unit -> 'a) -> 'a T
-  val fork: (unit -> 'a) -> 'a T
-  val fork_background: (unit -> 'a) -> 'a T
-  val join_results: 'a T list -> 'a Exn.result list
-  val join_result: 'a T -> 'a Exn.result
-  val join: 'a T -> 'a
+  val thread_data: unit -> (string * task) option
+  type 'a future
+  val task_of: 'a future -> task
+  val group_of: 'a future -> group
+  val peek: 'a future -> 'a Exn.result option
+  val is_finished: 'a future -> bool
+  val fork: (unit -> 'a) -> 'a future
+  val fork_group: group -> (unit -> 'a) -> 'a future
+  val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
+  val fork_background: (unit -> 'a) -> 'a future
+  val join_results: 'a future list -> 'a Exn.result list
+  val join_result: 'a future -> 'a Exn.result
+  val join: 'a future -> 'a
+  val map: ('a -> 'b) -> 'a future -> 'b future
   val focus: task list -> unit
   val interrupt_task: string -> unit
-  val cancel: 'a T -> unit
+  val cancel: 'a future -> unit
   val shutdown: unit -> unit
 end;
 
@@ -63,7 +65,7 @@
 type task = TaskQueue.task;
 type group = TaskQueue.group;
 
-local val tag = Universal.tag () : (string * task * group) option Universal.tag in
+local val tag = Universal.tag () : (string * task) option Universal.tag in
   fun thread_data () = the_default NONE (Thread.getLocal tag);
   fun setmp_thread_data data f x = Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
 end;
@@ -71,7 +73,7 @@
 
 (* datatype future *)
 
-datatype 'a T = Future of
+datatype 'a future = Future of
  {task: task,
   group: group,
   result: 'a Exn.result option ref};
@@ -140,7 +142,7 @@
 fun execute name (task, group, run) =
   let
     val _ = trace_active ();
-    val ok = setmp_thread_data (name, task, group) run ();
+    val ok = setmp_thread_data (name, task) run ();
     val _ = SYNCHRONIZED "execute" (fn () =>
      (change queue (TaskQueue.finish task);
       if ok then ()
@@ -246,10 +248,10 @@
       change_result queue (TaskQueue.enqueue group deps pri run) before notify_all ());
   in Future {task = task, group = group, result = result} end;
 
-fun fork_common pri = future (Option.map #3 (thread_data ())) [] pri;
-
-fun fork e = fork_common true e;
-fun fork_background e = fork_common false e;
+fun fork e = future NONE [] true e;
+fun fork_group group e = future (SOME group) [] true e;
+fun fork_deps deps e = future NONE (map task_of deps) true e;
+fun fork_background e = future NONE [] false e;
 
 
 (* join: retrieve results *)
@@ -274,7 +276,7 @@
               (*alien thread -- refrain from contending for resources*)
               while exists (not o is_finished) xs
               do SYNCHRONIZED "join_thread" (fn () => wait "join_thread")
-          | SOME (name, task, _) =>
+          | SOME (name, task) =>
               (*proper task -- actively work towards results*)
               let
                 val unfinished = xs |> map_filter
@@ -292,6 +294,8 @@
 fun join_result x = singleton join_results x;
 fun join x = Exn.release (join_result x);
 
+fun map f x = fork_deps [x] (fn () => f (join x));
+
 
 (* misc operations *)
 
@@ -324,3 +328,6 @@
   else ();
 
 end;
+
+type 'a future = 'a Future.future;
+
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -31,7 +31,7 @@
   if Future.enabled () then
     let
       val group = TaskQueue.new_group ();
-      val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
+      val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
       val _ = List.app (ignore o Future.join_result) futures;
     in Future.join_results futures end
   else map (Exn.capture f) xs;
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/General/lazy.ML
--- a/src/Pure/General/lazy.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/General/lazy.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -8,13 +8,13 @@
 
 signature LAZY =
 sig
-  type 'a T
-  val same: 'a T * 'a T -> bool
-  val lazy: (unit -> 'a) -> 'a T
-  val value: 'a -> 'a T
-  val peek: 'a T -> 'a Exn.result option
-  val force: 'a T -> 'a
-  val map_force: ('a -> 'a) -> 'a T -> 'a T
+  type 'a lazy
+  val same: 'a lazy * 'a lazy -> bool
+  val lazy: (unit -> 'a) -> 'a lazy
+  val value: 'a -> 'a lazy
+  val peek: 'a lazy -> 'a Exn.result option
+  val force: 'a lazy -> 'a
+  val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
 end
 
 structure Lazy :> LAZY =
@@ -22,13 +22,13 @@
 
 (* datatype *)
 
-datatype 'a lazy =
+datatype 'a T =
   Lazy of unit -> 'a |
   Result of 'a Exn.result;
 
-type 'a T = 'a lazy ref;
+type 'a lazy = 'a T ref;
 
-fun same (r1: 'a T, r2) = r1 = r2;
+fun same (r1: 'a lazy, r2) = r1 = r2;
 
 fun lazy e = ref (Lazy e);
 fun value x = ref (Result (Exn.Result x));
@@ -58,3 +58,6 @@
 fun map_force f = value o f o force;
 
 end;
+
+type 'a lazy = 'a Lazy.lazy;
+
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/Isar/code.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -15,7 +15,7 @@
   val add_default_eqn_attrib: Attrib.src
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
-  val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
+  val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
   val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
   val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
   val add_inline: thm -> theory -> theory
@@ -114,7 +114,7 @@
 
 (* defining equations *)
 
-type eqns = bool * (thm * bool) list Lazy.T;
+type eqns = bool * (thm * bool) list lazy;
   (*default flag, theorems with linear flag (perhaps lazy)*)
 
 fun pretty_lthms ctxt r = case Lazy.peek r
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -115,7 +115,7 @@
   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   val is_relevant: state -> bool
-  val future_proof: (state -> context) -> state -> context
+  val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
 end;
 
 structure Proof: PROOF =
@@ -990,7 +990,7 @@
   not (is_initial state) orelse
   schematic_goal state;
 
-fun future_proof make_proof state =
+fun future_proof proof state =
   let
     val _ = is_relevant state andalso error "Cannot fork relevant proof";
 
@@ -1004,16 +1004,19 @@
     fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [Goal.conclude th]);
     val this_name = ProofContext.full_bname (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
 
-    fun make_result () = state
+    val result_ctxt =
+      state
       |> map_contexts (Variable.auto_fixes prop)
       |> map_goal I (K (statement', messages, using, goal', before_qed, (#1 after_qed, after_qed')))
-      |> make_proof
-      |> (fn result_ctxt => ProofContext.get_fact_single result_ctxt (Facts.named this_name));
-    val finished_goal = Goal.protect (Goal.future_result goal_ctxt make_result prop);
-  in
-    state
-    |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
-    |> global_done_proof
-  end;
+      |> proof;
+
+    val thm = result_ctxt |> Future.map (fn (_, ctxt) =>
+      ProofContext.get_fact_single ctxt (Facts.named this_name));
+    val finished_goal = Goal.protect (Goal.future_result goal_ctxt thm prop);
+    val state' =
+      state
+      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
+      |> global_done_proof;
+  in (Future.map #1 result_ctxt, state') end;
 
 end;
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -691,45 +691,62 @@
 
 (* excursion of units, consisting of commands with proof *)
 
+structure States = ProofDataFun
+(
+  type T = state list future option;
+  fun init _ = NONE;
+);
+
 fun command_result tr st =
   let val st' = command tr st
   in (st', st') end;
 
-fun unit_result immediate (tr, proof_trs) st =
+fun proof_result immediate (tr, proof_trs) st =
   let val st' = command tr st in
     if immediate orelse null proof_trs orelse
       not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     then
       let val (states, st'') = fold_map command_result proof_trs st'
-      in (fn () => (tr, st') :: (proof_trs ~~ states), st'') end
+      in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end
     else
       let
         val (body_trs, end_tr) = split_last proof_trs;
-        val body_states = ref ([]: state list);
         val finish = Context.Theory o ProofContext.theory_of;
-        fun make_result prf =
-          let val (states, State (result_node, _)) =
-            (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
-              => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
-            |> fold_map command_result body_trs
-            ||> command (end_tr |> set_print false)
-          in body_states := states; presentation_context (Option.map #1 result_node) NONE end;
-        val st'' = st'
-          |> command (end_tr |> reset_trans |> end_proof (K (Proof.future_proof make_result)));
-      in (fn () => (tr, st') :: (body_trs ~~ ! body_states) @ [(end_tr, st'')], st'') end
+
+        val future_proof = Proof.future_proof
+          (fn prf =>
+            Future.fork_background (fn () =>
+              let val (states, State (result_node, _)) =
+                (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
+                  => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
+                |> fold_map command_result body_trs
+                ||> command (end_tr |> set_print false);
+              in (states, presentation_context (Option.map #1 result_node) NONE) end))
+          #> (fn (states, ctxt) => States.put (SOME states) ctxt);
+
+        val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
+
+        val states =
+          (case States.get (presentation_context (SOME (node_of st'')) NONE) of
+            NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
+          | SOME states => states);
+        val result = Lazy.lazy
+          (fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]);
+
+      in (result, st'') end
   end;
 
-fun excursion input =
+fun excursion input = exception_trace (fn () =>
   let
     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
 
     val immediate = not (Future.enabled ());
-    val (future_results, end_state) = fold_map (unit_result immediate) input toplevel;
+    val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
     val _ =
       (case end_state of
-        State (NONE, SOME (Theory (Context.Theory thy, _), _)) => Thm.join_futures thy
+        State (NONE, SOME (Theory (Context.Theory thy, _), _)) => PureThy.force_proofs thy
       | _ => error "Unfinished development at end of input");
-    val results = maps (fn res => res ()) future_results;
-  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end;
+    val results = maps Lazy.force future_results;
+  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);
 
 end;
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/ML-Systems/install_pp_polyml.ML
--- a/src/Pure/ML-Systems/install_pp_polyml.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -4,13 +4,13 @@
 Extra toplevel pretty-printing for Poly/ML.
 *)
 
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Future.T) =>
+install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
   (case Future.peek x of
     NONE => str "<future>"
   | SOME (Exn.Exn _) => str "<failed>"
   | SOME (Exn.Result y) => print (y, depth)));
 
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Lazy.T) =>
+install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
   (case Lazy.peek x of
     NONE => str "<lazy>"
   | SOME (Exn.Exn _) => str "<failed>"
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -320,14 +320,12 @@
     val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
       (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
 
-    val group = TaskQueue.new_group ();
     fun future (name, body) tab =
       let
         val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
-        val x = Future.future (SOME group) deps true body;
-      in (x, Symtab.update (name, Future.task_of x) tab) end;
+        val x = Future.fork_deps deps body;
+      in (x, Symtab.update (name, x) tab) end;
     val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
-    val _ = List.app (PureThy.force_proofs o get_theory o #1) tasks;
   in () end;
 
 local
@@ -589,8 +587,6 @@
 
 (* finish all theories *)
 
-fun finish () = change_thys (Graph.map_nodes
-  (fn (SOME _, SOME thy) => (NONE, (PureThy.force_proofs thy; SOME thy))
-    | (_, entry) => (NONE, entry)));
+fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
 
 end;
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/goal.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -20,7 +20,7 @@
   val conclude: thm -> thm
   val finish: thm -> thm
   val norm_result: thm -> thm
-  val future_result: Proof.context -> (unit -> thm) -> term -> thm
+  val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
@@ -116,11 +116,11 @@
 
     val global_prop =
       Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
-    val global_result =
-      Thm.generalize (map #1 tfrees, []) 0 o
-      Drule.forall_intr_list fixes o
-      Drule.implies_intr_list assms o
-      Thm.adjust_maxidx_thm ~1 o result;
+    val global_result = result |> Future.map
+      (Thm.adjust_maxidx_thm ~1 #>
+        Drule.implies_intr_list assms #>
+        Drule.forall_intr_list fixes #>
+        Thm.generalize (map #1 tfrees, []) 0);
     val local_result =
       Thm.future global_result (cert global_prop)
       |> Thm.instantiate (instT, [])
@@ -178,7 +178,7 @@
           end);
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
-      else future_result ctxt' result (Thm.term_of stmt);
+      else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -22,10 +22,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.T)
+   | PThm of serial * ((string * term * typ list option) * proof_body lazy)
   and proof_body = PBody of
     {oracles: (string * term) OrdList.T,
-     thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
+     thms: (serial * (string * term * proof_body lazy)) OrdList.T,
      proof: proof}
 
   val %> : proof * term -> proof
@@ -36,10 +36,10 @@
   include BASIC_PROOFTERM
 
   type oracle = string * term
-  type pthm = serial * (string * term * proof_body Lazy.T)
-  val force_body: proof_body Lazy.T ->
+  type pthm = serial * (string * term * proof_body lazy)
+  val force_body: proof_body lazy ->
     {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
-  val force_proof: proof_body Lazy.T -> proof
+  val force_proof: proof_body lazy -> 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
@@ -111,7 +111,7 @@
   val promise_proof: theory -> serial -> term -> proof
   val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> term list -> term ->
-    (serial * proof) list Lazy.T -> proof_body -> pthm * proof
+    (serial * proof) list lazy -> proof_body -> pthm * proof
   val get_name: term list -> term -> proof -> string
 
   (** rewriting on proof terms **)
@@ -143,14 +143,14 @@
  | 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.T)
+ | PThm of serial * ((string * term * typ list option) * proof_body lazy)
 and proof_body = PBody of
   {oracles: (string * term) OrdList.T,
-   thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
+   thms: (serial * (string * term * proof_body lazy)) OrdList.T,
    proof: proof};
 
 type oracle = string * term;
-type pthm = serial * (string * term * proof_body Lazy.T);
+type pthm = serial * (string * term * proof_body lazy);
 
 val force_body = Lazy.force #> (fn PBody args => args);
 val force_proof = #proof o force_body;
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/pure_thy.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -59,7 +59,7 @@
 
 structure FactsData = TheoryDataFun
 (
-  type T = Facts.T * unit Lazy.T list;
+  type T = Facts.T * unit lazy list;
   val empty = (Facts.empty, []);
   val copy = I;
   fun extend (facts, _) = (facts, []);
@@ -80,7 +80,9 @@
 (* proofs *)
 
 fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
-val force_proofs = List.app Lazy.force o #2 o FactsData.get;
+
+fun force_proofs thy =
+  ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
 
 
 
diff -r 694227dd3e8c -r c4ae153d78ab src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Pure/thm.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -146,8 +146,7 @@
   val varifyT: thm -> thm
   val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val freezeT: thm -> thm
-  val join_futures: theory -> unit
-  val future: (unit -> thm) -> cterm -> thm
+  val future: thm future -> cterm -> thm
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
   val force_proof: thm -> unit
@@ -347,8 +346,8 @@
   tpairs: (term * term) list,                   (*flex-flex pairs*)
   prop: term}                                   (*conclusion*)
 and deriv = Deriv of
- {all_promises: (serial * thm Future.T) OrdList.T,
-  promises: (serial * thm Future.T) OrdList.T,
+ {all_promises: (serial * thm future) OrdList.T,
+  promises: (serial * thm future) OrdList.T,
   body: Pt.proof_body};
 
 type conv = cterm -> thm;
@@ -1587,36 +1586,7 @@
 
 
 
-(*** Promises ***)
-
-(* pending future derivations *)
-
-structure Futures = TheoryDataFun
-(
-  type T = thm Future.T list ref;
-  val empty : T = ref [];
-  val copy = I;  (*shared ref within all versions of whole theory body*)
-  fun extend _ : T = ref [];
-  fun merge _ _ : T = ref [];
-);
-
-val _ = Context.>> (Context.map_theory Futures.init);
-
-fun add_future thy future = CRITICAL (fn () => change (Futures.get thy) (cons future));
-
-fun join_futures thy =
-  let
-    val futures = Futures.get thy;
-    fun joined () =
-     (List.app (ignore o Future.join_result) (rev (! futures));
-      CRITICAL (fn () =>
-        let
-          val (finished, unfinished) = List.partition Future.is_finished (! futures);
-          val _ = futures := unfinished;
-        in finished end)
-      |> Future.join_results |> Exn.release_all |> null);
-  in while not (joined ()) do () end;
-
+(*** Future theorems -- proofs with promises ***)
 
 (* future rule *)
 
@@ -1635,15 +1605,14 @@
     val _ = forall (fn (j, _) => j < i) all_promises orelse err "bad dependencies";
   in thm end;
 
-fun future make_result ct =
+fun future future_thm ct =
   let
     val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
     val thy = Context.reject_draft (Theory.deref thy_ref);
     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
 
     val i = serial ();
-    val future = Future.fork_background (future_result i thy sorts prop o norm_proof o make_result);
-    val _ = add_future thy future;
+    val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof);
     val promise = (i, future);
   in
     Thm (make_deriv [promise] [promise] [] [] (Pt.promise_proof thy i prop),
diff -r 694227dd3e8c -r c4ae153d78ab src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Fri Dec 05 08:04:53 2008 +0100
+++ b/src/Tools/code/code_ml.ML	Fri Dec 05 08:05:14 2008 +0100
@@ -912,7 +912,7 @@
 
 structure CodeAntiqData = ProofDataFun
 (
-  type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));
+  type T = string list * (bool * (string * (string * (string * string) list) lazy));
   fun init _ = ([], (true, ("", Lazy.value ("", []))));
 );