# HG changeset patch
# User wenzelm
# Date 1703010021 -3600
# Node ID e4a9a861856bbc8958e17611a5145f39b6ec19f8
# Parent  dc6b58da806ea67e17dfbc44ce435ed360eea68e
omit pointless future: proof terms are built sequentially;

diff -r dc6b58da806e -r e4a9a861856b src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 19 19:18:09 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 19 19:20:21 2023 +0100
@@ -259,7 +259,7 @@
   val norm_type: Type.tyenv -> ztyp -> ztyp
   val norm_term: theory -> Envir.env -> zterm -> zterm
   val norm_proof: theory -> Envir.env -> term list -> zproof -> zproof
-  type zbox = serial * (zterm * zproof future)
+  type zbox = serial * (zterm * zproof)
   val zbox_ord: zbox ord
   type zboxes = zbox Ord_List.T
   val union_zboxes: zboxes -> zboxes -> zboxes
@@ -753,7 +753,7 @@
 
 (* closed proof boxes *)
 
-type zbox = serial * (zterm * zproof future);
+type zbox = serial * (zterm * zproof);
 val zbox_ord: zbox ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
 type zboxes = zbox Ord_List.T;
@@ -796,7 +796,7 @@
     val prf' = beta_norm_prooft (close_proof hyps' prf);
 
     val i = serial ();
-    val zboxes' = add_zboxes (i, (prop', Future.value prf')) zboxes;
+    val zboxes' = add_zboxes (i, (prop', prf')) zboxes;
     val prf'' = ZAppts (ZConstp (zproof_const (ZBox i) prop'), hyps');
   in (zboxes', prf'') end;