# HG changeset patch
# User wenzelm
# Date 1701544916 -3600
# Node ID 0c7de2ae814b7518fc42f572ad9c9f48cd657b2d
# Parent  ff68cbfa3550adccc84963b151cf75f6546321d6# Parent  686b7b14d041bab75617275ac1f0c40c310ed8e4
merged

diff -r ff68cbfa3550 -r 0c7de2ae814b src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -227,7 +227,7 @@
   end;
 
 fun add_dt_realizers config names thy =
-  if not (Proofterm.proofs_enabled ()) then thy
+  if not (Proofterm.proof_enabled (! Proofterm.proofs)) then thy
   else
     let
       val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
diff -r ff68cbfa3550 -r 0c7de2ae814b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -1339,7 +1339,7 @@
 
 fun future_terminal_proof proof1 proof2 done state =
   if Future.proofs_enabled 3 andalso
-    not (Proofterm.proofs_enabled ()) andalso
+    not (Proofterm.any_proofs_enabled ()) andalso
     not (is_relevant state)
   then
     state |> future_proof (fn state' =>
diff -r ff68cbfa3550 -r 0c7de2ae814b src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -734,7 +734,7 @@
   (case try proof_of st of
     NONE => false
   | SOME state =>
-      not (Proofterm.proofs_enabled ()) andalso
+      not (Proofterm.any_proofs_enabled ()) andalso
       not (Proof.is_relevant state) andalso
        (if can (Proof.assert_bottom true) state
         then Future.proofs_enabled 1
diff -r ff68cbfa3550 -r 0c7de2ae814b src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -184,7 +184,8 @@
       PBody
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
-        proof = prf};
+        zboxes = Proofterm.empty_zboxes,
+        proof = (prf, ZDummy)};
   in Proofterm.thm_body body end;
 
 
diff -r ff68cbfa3550 -r 0c7de2ae814b src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/Pure/ROOT.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -168,15 +168,15 @@
 ML_file "item_net.ML";
 ML_file "envir.ML";
 ML_file "consts.ML";
-ML_file "zterm.ML";
-ML_file "term_xml.ML";
 ML_file "primitive_defs.ML";
 ML_file "sign.ML";
 ML_file "defs.ML";
-ML_file "term_sharing.ML";
 ML_file "pattern.ML";
 ML_file "unify.ML";
 ML_file "theory.ML";
+ML_file "term_sharing.ML";
+ML_file "term_xml.ML";
+ML_file "zterm.ML";
 ML_file "proofterm.ML";
 ML_file "thm.ML";
 ML_file "cterm_items.ML";
diff -r ff68cbfa3550 -r 0c7de2ae814b src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/Pure/global_theory.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -277,7 +277,7 @@
   end;
 
 fun check_thms_lazy (thms: thm list lazy) =
-  if Proofterm.proofs_enabled () orelse Options.default_bool "strict_facts"
+  if Proofterm.any_proofs_enabled () orelse Options.default_bool "strict_facts"
   then Lazy.force_value thms else thms;
 
 fun add_thms_lazy kind (b, thms) thy =
diff -r ff68cbfa3550 -r 0c7de2ae814b src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/Pure/goal.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -101,7 +101,7 @@
 
 fun skip_proofs_enabled () =
   let val skip = Options.default_bool "skip_proofs" in
-    if Proofterm.proofs_enabled () andalso skip then
+    if Proofterm.any_proofs_enabled () andalso skip then
       (warning "Proof terms enabled -- cannot skip proofs"; false)
     else skip
   end;
@@ -166,7 +166,7 @@
 
     val schematic = exists Term.is_schematic props;
     val immediate = is_none fork_pri;
-    val future = Future.proofs_enabled 1 andalso not (Proofterm.proofs_enabled ());
+    val future = Future.proofs_enabled 1 andalso not (Proofterm.any_proofs_enabled ());
     val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
 
     val pos = Position.thread_data ();
diff -r ff68cbfa3550 -r 0c7de2ae814b src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/Pure/proofterm.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -13,6 +13,7 @@
       prop: term, types: typ list option}
   type thm_body
   type thm_node
+  type zboxes = (zterm * zproof future) Inttab.table
   datatype proof =
      MinProof
    | PBound of int
@@ -28,13 +29,17 @@
   and proof_body = PBody of
     {oracles: ((string * Position.T) * term option) Ord_List.T,
      thms: (serial * thm_node) Ord_List.T,
-     proof: proof}
+     zboxes: zboxes,
+     proof: proof * zproof}
+  type proofs = proof * zproof
   type oracle = (string * Position.T) * term option
   type thm = serial * thm_node
   exception MIN_PROOF of unit
+  val proofs_of: proof_body -> proofs
   val proof_of: proof_body -> proof
+  val zproof_of: proof_body -> zproof
   val join_proof: proof_body future -> proof
-  val map_proof_of: (proof -> proof) -> proof_body -> proof_body
+  val map_proofs_of: (proofs -> proofs) -> proof_body -> proof_body
   val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option ->
     thm_header
   val thm_body: proof_body -> thm_body
@@ -57,7 +62,10 @@
   val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
   val union_thms: thm Ord_List.T -> thm Ord_List.T -> thm Ord_List.T
   val unions_thms: thm Ord_List.T list -> thm Ord_List.T
-  val no_proof_body: proof -> proof_body
+  val empty_zboxes: zboxes
+  val union_zboxes: zboxes -> zboxes -> zboxes
+  val no_proof: proofs
+  val no_proof_body: proofs -> proof_body
   val no_thm_names: proof -> proof
   val no_thm_proofs: proof -> proof
   val no_body_proofs: proof -> proof
@@ -72,8 +80,10 @@
   val %> : proof * term -> proof
 
   (*primitive operations*)
+  val proof_enabled: int -> bool
+  val zproof_enabled: int -> bool
   val proofs: int Unsynchronized.ref
-  val proofs_enabled: unit -> bool
+  val any_proofs_enabled: unit -> bool
   val atomic_proof: proof -> bool
   val compact_proof: proof -> bool
   val proof_combt: proof * term list -> proof
@@ -137,6 +147,7 @@
   val equal_elim_proof: term -> term -> proof -> proof -> proof
   val abstract_rule_proof: string * term -> proof -> proof
   val combination_proof: term -> term -> term -> term -> proof -> proof -> proof
+  val could_unify: proof * proof -> bool
   val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
     sort list -> proof -> proof
   val of_sort_proof: Sorts.algebra ->
@@ -206,6 +217,8 @@
   {serial: serial, pos: Position.T list, theory_name: string, name: string,
     prop: term, types: typ list option};
 
+type zboxes = (zterm * zproof future) Inttab.table;
+
 datatype proof =
    MinProof
  | PBound of int
@@ -221,13 +234,16 @@
 and proof_body = PBody of
   {oracles: ((string * Position.T) * term option) Ord_List.T,
    thms: (serial * thm_node) Ord_List.T,
-   proof: proof}
+   zboxes: zboxes,
+   proof: proof * zproof}
 and thm_body =
   Thm_Body of {open_proof: proof -> proof, body: proof_body future}
 and thm_node =
   Thm_Node of {theory_name: string, name: string, prop: term,
     body: proof_body future, export: unit lazy, consolidate: unit lazy};
 
+type proofs = proof * zproof;
+
 type oracle = (string * Position.T) * term option;
 val oracle_ord: oracle ord =
   prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord);
@@ -238,11 +254,13 @@
 
 exception MIN_PROOF of unit;
 
-fun proof_of (PBody {proof, ...}) = proof;
+fun proofs_of (PBody {proof, ...}) = proof;
+val proof_of = fst o proofs_of;
+val zproof_of = snd o proofs_of;
 val join_proof = Future.join #> proof_of;
 
-fun map_proof_of f (PBody {oracles, thms, proof}) =
-  PBody {oracles = oracles, thms = thms, proof = f proof};
+fun map_proofs_of f (PBody {oracles, thms, zboxes, proof}) =
+  PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = f proof};
 
 fun thm_header serial pos theory_name name prop types : thm_header =
   {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
@@ -324,8 +342,12 @@
 val union_thms = Ord_List.union thm_ord;
 val unions_thms = Ord_List.unions thm_ord;
 
-fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
-val no_thm_body = thm_body (no_proof_body MinProof);
+val empty_zboxes: zboxes = Inttab.empty;
+val union_zboxes = curry (Inttab.merge (fn (_: (zterm * zproof future), _) => true));
+
+val no_proof = (MinProof, ZDummy);
+fun no_proof_body proof = PBody {oracles = [], thms = [], zboxes = empty_zboxes, proof = proof};
+val no_thm_body = thm_body (no_proof_body no_proof);
 
 fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
   | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
@@ -348,7 +370,7 @@
   | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2
   | no_body_proofs (PThm (header, Thm_Body {open_proof, body})) =
       let
-        val body' = Future.value (no_proof_body (join_proof body));
+        val body' = Future.value (no_proof_body (proofs_of (Future.join body)));
         val thm_body' = Thm_Body {open_proof = open_proof, body = body'};
       in PThm (header, thm_body') end
   | no_body_proofs a = a;
@@ -377,8 +399,9 @@
   fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
     ([int_atom serial, theory_name, name],
       pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
-        (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
-and proof_body consts (PBody {oracles, thms, proof = prf}) =
+        (map Position.properties_of pos,
+          (prop, (types, map_proofs_of (apfst open_proof) (Future.join body)))))]
+and proof_body consts (PBody {oracles, thms, zboxes = _, proof = (prf, _)}) =
   triple (list (pair (pair string (properties o Position.properties_of))
       (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
 and thm consts (a, thm_node) =
@@ -446,7 +469,7 @@
     val (a, b, c) =
       triple (list (pair (pair string (Position.of_properties o properties))
         (option (term consts)))) (list (thm consts)) (proof consts) x;
-  in PBody {oracles = a, thms = b, proof = c} end
+  in PBody {oracles = a, thms = b, zboxes = empty_zboxes, proof = (c, ZDummy)} end
 and thm consts x =
   let
     val (a, (b, (c, (d, e)))) =
@@ -463,8 +486,14 @@
 
 (** proof objects with different levels of detail **)
 
-val proofs = Unsynchronized.ref 2;
-fun proofs_enabled () = ! proofs >= 2;
+fun proof_enabled proofs = Word.andb (Word.fromInt proofs, 0w2) <> 0w0;
+fun zproof_enabled proofs = Word.andb (Word.fromInt proofs, 0w4) <> 0w0;
+
+val proofs = Unsynchronized.ref 6;
+
+fun any_proofs_enabled () =
+  let val proofs = ! proofs
+  in proof_enabled proofs orelse zproof_enabled proofs end;
 
 fun atomic_proof prf =
   (case prf of
@@ -495,7 +524,7 @@
           | stripc  x =  x
     in  stripc (prf, [])  end;
 
-fun strip_thm_body (body as PBody {proof, ...}) =
+fun strip_thm_body (body as PBody {proof = (proof, _), ...}) =
   (case fst (strip_combt (fst (strip_combP proof))) of
     PThm (_, Thm_Body {body = body', ...}) => Future.join body'
   | _ => body);
@@ -1463,10 +1492,10 @@
 
 (*A fast unification filter: true unless the two terms cannot be unified.
   Terms must be NORMAL.  Treats all Vars as distinct. *)
-fun could_unify prf1 prf2 =
+fun could_unify (prf1, prf2) =
   let
     fun matchrands (prf1 %% prf2) (prf1' %% prf2') =
-          could_unify prf2 prf2' andalso matchrands prf1 prf1'
+          could_unify (prf2, prf2') andalso matchrands prf1 prf1'
       | matchrands (prf % SOME t) (prf' % SOME t') =
           Term.could_unify (t, t') andalso matchrands prf prf'
       | matchrands (prf % _) (prf' % _) = matchrands prf prf'
@@ -1505,7 +1534,7 @@
           (case get_first (fn r => r Ts hs prf) procs of
             NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
               (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
-                 handle PMatch => NONE) (filter (could_unify prf o fst) rules)
+                 handle PMatch => NONE) (filter (fn (prf', _) => could_unify (prf, prf')) rules)
           | some => some);
 
     fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) =
@@ -1604,7 +1633,7 @@
   let val (rules, procs) = #1 (Data.get thy)
   in (map #2 rules, map #2 procs) end;
 
-fun rew_proof thy = rewrite_prf fst (get_rew_data thy);
+fun rew_proof thy prf = rewrite_prf fst (get_rew_data thy) prf;
 
 fun add_prf_rrule r = (Data.map o apfst o apfst) (cons (stamp (), r));
 fun add_prf_rproc p = (Data.map o apfst o apsnd) (cons (stamp (), p));
@@ -1993,14 +2022,17 @@
 fun fulfill_norm_proof thy ps body0 =
   let
     val _ = consolidate_bodies (map #2 ps @ [body0]);
-    val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
+    val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (proof0, zproof)} = body0;
     val oracles =
       unions_oracles
         (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
     val thms =
       unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
+    val zboxes = fold (fn (_, PBody {zboxes, ...}) => union_zboxes zboxes) ps zboxes0;
     val proof = rew_proof thy proof0;
-  in PBody {oracles = oracles, thms = thms, proof = proof} end;
+  in
+    PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = (proof, zproof)}
+  end;
 
 fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body =
   let
@@ -2130,7 +2162,7 @@
 
 fun prune_body body =
   if Options.default_bool "prune_proofs"
-  then (Future.map o map_proof_of) (K MinProof) body
+  then (Future.map o map_proofs_of) (K no_proof) body
   else body;
 
 fun export_enabled () = Options.default_bool "export_proofs";
@@ -2208,19 +2240,19 @@
 
     val (ucontext, prop1) = Logic.unconstrainT shyps prop;
 
-    val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
-    val body0 =
-      Future.value
-        (PBody {oracles = oracles0, thms = thms0,
-          proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof});
+    val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf, zprf)} = body;
+    val proofs = ! proofs;
+    val prf' = if proof_enabled proofs then fold_rev implies_intr_proof hyps prf else MinProof;
+    val zprf' = if zproof_enabled proofs then ZTerm.todo_proof zprf else ZDummy;
+    val body0 = PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf', zprf')};
 
     fun new_prf () =
       let
         val i = serial ();
         val unconstrainT =
           unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
-        val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
-      in (i, fulfill_proof_future thy promises postproc body0) end;
+        val postproc = map_proofs_of (apfst (unconstrainT #> named ? rew_proof thy));
+      in (i, fulfill_proof_future thy promises postproc (Future.value body0)) end;
 
     val (i, body') =
       (*somewhat non-deterministic proof boxes!*)
@@ -2232,7 +2264,7 @@
               let
                 val Thm_Body {body = body', ...} = thm_body';
                 val i = if a = "" andalso named then serial () else ser;
-              in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
+              in (i, body' |> ser <> i ? Future.map (map_proofs_of (apfst (rew_proof thy)))) end
             else new_prf ()
         | _ => new_prf ());
 
diff -r ff68cbfa3550 -r 0c7de2ae814b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/Pure/thm.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -744,10 +744,11 @@
 
 (** derivations and promised proofs **)
 
-fun make_deriv promises oracles thms proof =
-  Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
+fun make_deriv promises oracles thms zboxes proof =
+  Deriv {promises = promises,
+    body = PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = proof}};
 
-val empty_deriv = make_deriv [] [] [] MinProof;
+val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes Proofterm.no_proof;
 
 
 (* inference rules *)
@@ -757,29 +758,42 @@
 fun bad_proofs i =
   error ("Illegal level of detail for proof objects: " ^ string_of_int i);
 
-fun deriv_rule2 f
-    (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}})
-    (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) =
+fun deriv_rule2 (f, g)
+    (Deriv {promises = ps1, body = body1}) (Deriv {promises = ps2, body = body2}) =
   let
     val ps = Ord_List.union promise_ord ps1 ps2;
+
+    val PBody {oracles = oracles1, thms = thms1, zboxes = zboxes1, proof = (prf1, zprf1)} = body1;
+    val PBody {oracles = oracles2, thms = thms2, zboxes = zboxes2, proof = (prf2, zprf2)} = body2;
+
     val oracles = Proofterm.union_oracles oracles1 oracles2;
     val thms = Proofterm.union_thms thms1 thms2;
-    val prf =
+    val zboxes = Proofterm.union_zboxes zboxes1 zboxes2;
+    val proof =
       (case ! Proofterm.proofs of
-        2 => f prf1 prf2
-      | 1 => MinProof
-      | 0 => MinProof
+        0 => Proofterm.no_proof
+      | 1 => Proofterm.no_proof
+      | 2 => (f prf1 prf2, ZDummy)
+      | 4 => (MinProof, g zprf1 zprf2)
+      | 5 => (MinProof, g zprf1 zprf2)
+      | 6 => (f prf1 prf2, g zprf1 zprf2)
       | i => bad_proofs i);
-  in make_deriv ps oracles thms prf end;
+  in make_deriv ps oracles thms zboxes proof end;
 
-fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
+fun deriv_rule1 (f, g) = deriv_rule2 (K f, K g) empty_deriv;
 
-fun deriv_rule0 make_prf =
-  if ! Proofterm.proofs <= 1 then empty_deriv
-  else deriv_rule1 I (make_deriv [] [] [] (make_prf ()));
+fun deriv_rule0 (f, g) =
+  let val proofs = ! Proofterm.proofs in
+    if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
+      deriv_rule1 (I, I) (make_deriv [] [] [] Proofterm.empty_zboxes
+       (if Proofterm.proof_enabled proofs then f () else MinProof,
+        if Proofterm.zproof_enabled proofs then g () else ZDummy))
+    else empty_deriv
+  end;
 
-fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
-  make_deriv promises oracles thms (f proof);
+fun deriv_rule_unconditional (f, g)
+    (Deriv {promises, body = PBody {oracles, thms, zboxes, proof = (prf, zprf)}}) =
+  make_deriv promises oracles thms zboxes (f prf, g zprf);
 
 
 (* fulfilled proofs *)
@@ -833,13 +847,13 @@
     val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct;
     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
     val _ =
-      if Proofterm.proofs_enabled ()
+      if Proofterm.any_proofs_enabled ()
       then raise CTERM ("future: proof terms enabled", [ct]) else ();
 
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in
-    Thm (make_deriv [(i, future)] [] [] MinProof,
+    Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes Proofterm.no_proof,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -858,7 +872,7 @@
   (case Name_Space.lookup (Theory.axiom_table thy) name of
     SOME prop =>
       let
-        val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop);
+        val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop, ZTerm.todo_proof);
         val cert = Context.Certificate thy;
         val maxidx = maxidx_of_term prop;
         val shyps = Sorts.insert_term prop [];
@@ -885,7 +899,7 @@
 (* technical adjustments *)
 
 fun norm_proof (th as Thm (der, args)) =
-  Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th)) der, args);
+  Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th), I) der, args);
 
 fun adjust_maxidx_thm i
     (th as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
@@ -979,20 +993,24 @@
 
 local
 
-fun union_digest (oracles1, thms1) (oracles2, thms2) =
-  (Proofterm.union_oracles oracles1 oracles2, Proofterm.union_thms thms1 thms2);
+val empty_digest = ([], [], Proofterm.empty_zboxes);
 
-fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
-  (oracles, thms);
+fun union_digest (oracles1, thms1, zboxes1) (oracles2, thms2, zboxes2) =
+ (Proofterm.union_oracles oracles1 oracles2,
+  Proofterm.union_thms thms1 thms2,
+  Proofterm.union_zboxes zboxes1 zboxes2);
+
+fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, zboxes, ...}, ...}, _)) =
+  (oracles, thms, zboxes);
 
 fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
   Sorts.of_sort_derivation (Sign.classes_of thy)
    {class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 =>
-      if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
+      if c1 = c2 then empty_digest else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
     type_constructor = fn (a, _) => fn dom => fn c =>
       let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c))
       in (fold o fold) (union_digest o #1) dom arity_digest end,
-    type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)}
+    type_variable = fn T => map (pair empty_digest) (Type.sort_of_atyp T)}
    (typ, sort);
 
 in
@@ -1013,10 +1031,10 @@
             raise THEORY ("solve_constraints: bad theories for theorem\n" ^
               Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys);
 
-        val Deriv {promises, body = PBody {oracles, thms, proof}} = der;
-        val (oracles', thms') = (oracles, thms)
+        val Deriv {promises, body = PBody {oracles, thms, zboxes, proof}} = der;
+        val (oracles', thms', zboxes') = (oracles, thms, zboxes)
           |> fold (fold union_digest o constraint_digest) constraints;
-        val body' = PBody {oracles = oracles', thms = thms', proof = proof};
+        val body' = PBody {oracles = oracles', thms = thms', zboxes = zboxes', proof = proof};
       in
         Thm (Deriv {promises = promises, body = body'},
           {constraints = [], cert = cert, tags = tags, maxidx = maxidx,
@@ -1063,7 +1081,7 @@
         val shyps' = fold (Sorts.insert_sort o #2) present extra';
       in
         Thm (deriv_rule_unconditional
-          (Proofterm.strip_shyps_proof algebra present witnessed extra') der,
+          (Proofterm.strip_shyps_proof algebra present witnessed extra', I) der,
          {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
       end)
@@ -1117,10 +1135,11 @@
       val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
-      val (pthm, proof) =
+      val (pthm, prf) =
         Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
           name_pos shyps hyps prop ps body;
-      val der' = make_deriv [] [] [pthm] proof;
+      val zprf = ZTerm.todo_proof (Proofterm.zproof_of body);
+      val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf);
     in Thm (der', args) end);
 
 fun close_derivation pos =
@@ -1144,14 +1163,19 @@
           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
         else
           let
-            val (oracle, prf) =
+            fun no_oracle () = ((name, Position.none), NONE);
+            fun make_oracle () = ((name, Position.thread_data ()), SOME prop);
+            val (oracle, proof) =
               (case ! Proofterm.proofs of
-                2 => (((name, Position.thread_data ()), SOME prop), Proofterm.oracle_proof name prop)
-              | 1 => (((name, Position.thread_data ()), SOME prop), MinProof)
-              | 0 => (((name, Position.none), NONE), MinProof)
+                0 => (no_oracle (), Proofterm.no_proof)
+              | 1 => (make_oracle (), Proofterm.no_proof)
+              | 2 => (make_oracle (), (Proofterm.oracle_proof name prop, ZDummy))
+              | 4 => (no_oracle (), (MinProof, ZTerm.todo_proof ()))
+              | 5 => (make_oracle (), (MinProof, ZTerm.todo_proof ()))
+              | 6 => (make_oracle (), (Proofterm.oracle_proof name prop, ZTerm.todo_proof ()))
               | i => bad_proofs i);
           in
-            Thm (make_deriv [] [oracle] [] prf,
+            Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes proof,
              {cert = Context.join_certificate (Context.Certificate thy', cert2),
               tags = [],
               maxidx = maxidx,
@@ -1188,7 +1212,7 @@
       raise THM ("assume: prop", 0, [])
     else if maxidx <> ~1 then
       raise THM ("assume: variables", maxidx, [])
-    else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop),
+    else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop, ZTerm.todo_proof),
      {cert = cert,
       tags = [],
       maxidx = ~1,
@@ -1212,7 +1236,7 @@
   if T <> propT then
     raise THM ("implies_intr: assumptions must have type prop", 0, [th])
   else
-    Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,
+    Thm (deriv_rule1 (Proofterm.implies_intr_proof A, ZTerm.todo_proof) der,
      {cert = join_certificate1 (ct, th),
       tags = [],
       maxidx = Int.max (maxidx1, maxidx2),
@@ -1239,7 +1263,7 @@
     (case prop of
       Const ("Pure.imp", _) $ A $ B =>
         if A aconv propA then
-          Thm (deriv_rule2 (curry Proofterm.%%) der derA,
+          Thm (deriv_rule2 (curry Proofterm.%%, K ZTerm.todo_proof) der derA,
            {cert = join_certificate2 (thAB, thA),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1271,7 +1295,7 @@
       if occs x ts tpairs then
         raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
       else
-        Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE) der,
+        Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE, ZTerm.todo_proof) der,
          {cert = join_certificate1 (ct, th),
           tags = [],
           maxidx = Int.max (maxidx1, maxidx2),
@@ -1300,7 +1324,7 @@
       if T <> qary then
         raise THM ("forall_elim: type mismatch", 0, [th])
       else
-        Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,
+        Thm (deriv_rule1 (Proofterm.% o rpair (SOME t), ZTerm.todo_proof) der,
          {cert = join_certificate1 (ct, th),
           tags = [],
           maxidx = Int.max (maxidx1, maxidx2),
@@ -1318,7 +1342,7 @@
   t \<equiv> t
 *)
 fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
+  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
    {cert = cert,
     tags = [],
     maxidx = maxidx,
@@ -1336,7 +1360,7 @@
 fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
   (case prop of
     (eq as Const ("Pure.eq", _)) $ t $ u =>
-      Thm (deriv_rule1 Proofterm.symmetric_proof der,
+      Thm (deriv_rule1 (Proofterm.symmetric_proof, ZTerm.todo_proof) der,
        {cert = cert,
         tags = [],
         maxidx = maxidx,
@@ -1364,7 +1388,7 @@
       ((eq as Const ("Pure.eq", Type (_, [U, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
         if not (u aconv u') then err "middle term"
         else
-          Thm (deriv_rule2 (Proofterm.transitive_proof U u) der1 der2,
+          Thm (deriv_rule2 (Proofterm.transitive_proof U u, K ZTerm.todo_proof) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1387,7 +1411,7 @@
       (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
       | _ => raise THM ("beta_conversion: not a redex", 0, []));
   in
-    Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
+    Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1399,7 +1423,7 @@
   end;
 
 fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
+  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
    {cert = cert,
     tags = [],
     maxidx = maxidx,
@@ -1410,7 +1434,7 @@
     prop = Logic.mk_equals (t, Envir.eta_contract t)});
 
 fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
+  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
    {cert = cert,
     tags = [],
     maxidx = maxidx,
@@ -1436,7 +1460,7 @@
       if occs x ts tpairs then
         raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th])
       else
-        Thm (deriv_rule1 (Proofterm.abstract_rule_proof (b, x)) der,
+        Thm (deriv_rule1 (Proofterm.abstract_rule_proof (b, x), ZTerm.todo_proof) der,
          {cert = cert,
           tags = [],
           maxidx = maxidx,
@@ -1476,7 +1500,7 @@
       (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
        Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
         (chktypes fT tT;
-          Thm (deriv_rule2 (Proofterm.combination_proof f g t u) der1 der2,
+          Thm (deriv_rule2 (Proofterm.combination_proof f g t u, K ZTerm.todo_proof) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1504,7 +1528,7 @@
     (case (prop1, prop2) of
       (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
         if A aconv A' andalso B aconv B' then
-          Thm (deriv_rule2 (Proofterm.equal_intr_proof A B) der1 der2,
+          Thm (deriv_rule2 (Proofterm.equal_intr_proof A B, K ZTerm.todo_proof) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1533,7 +1557,7 @@
     (case prop1 of
       Const ("Pure.eq", _) $ A $ B =>
         if prop2 aconv A then
-          Thm (deriv_rule2 (Proofterm.equal_elim_proof A B) der1 der2,
+          Thm (deriv_rule2 (Proofterm.equal_elim_proof A B, K ZTerm.todo_proof) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1568,7 +1592,7 @@
               val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
                 (*remove trivial tpairs, of the form t \<equiv> t*)
                 |> filter_out (op aconv);
-              val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
+              val der' = deriv_rule1 (Proofterm.norm_proof' env, ZTerm.todo_proof) der;
               val thy' = Context.certificate_theory cert' handle ERROR msg =>
                 raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);
               val constraints' = insert_constraints_env thy' env constraints;
@@ -1612,7 +1636,7 @@
       val tpairs' = map (apply2 generalize) tpairs;
       val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
     in
-      Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der,
+      Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop, ZTerm.todo_proof) der,
        {cert = cert,
         tags = [],
         maxidx = maxidx',
@@ -1718,7 +1742,8 @@
           instT' constraints;
     in
       Thm (deriv_rule1
-        (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d) der,
+        (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d,
+          ZTerm.todo_proof) der,
        {cert = cert',
         tags = [],
         maxidx = maxidx',
@@ -1759,7 +1784,7 @@
   if T <> propT then
     raise THM ("trivial: the term must have type prop", 0, [])
   else
-    Thm (deriv_rule0 (fn () => Proofterm.trivial_proof),
+    Thm (deriv_rule0 (fn () => Proofterm.trivial_proof, ZTerm.todo_proof),
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1783,7 +1808,7 @@
     val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c));
   in
     if Sign.of_sort thy (T, [c]) then
-      Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c)),
+      Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c), ZTerm.todo_proof),
        {cert = cert,
         tags = [],
         maxidx = maxidx,
@@ -1810,10 +1835,11 @@
       val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
-      val (pthm, proof) =
+      val (pthm, prf) =
         Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
           shyps prop ps body;
-      val der' = make_deriv [] [] [pthm] proof;
+      val zprf = ZTerm.todo_proof body;
+      val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf);
       val prop' = Proofterm.thm_node_prop (#2 pthm);
     in
       Thm (der',
@@ -1835,7 +1861,7 @@
     val (al, prop2) = Type.varify_global tfrees prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
-    (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der,
+    (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees, ZTerm.todo_proof) der,
      {cert = cert,
       tags = [],
       maxidx = Int.max (0, maxidx),
@@ -1855,7 +1881,7 @@
     val prop2 = Type.legacy_freeze prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
-    Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der,
+    Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1, ZTerm.todo_proof) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx_of_term prop2,
@@ -1904,7 +1930,7 @@
   in
     if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
     else
-      Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der,
+      Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop, ZTerm.todo_proof) der,
        {cert = join_certificate1 (goal, orule),
         tags = [],
         maxidx = maxidx + inc,
@@ -1919,7 +1945,7 @@
   if i < 0 then raise THM ("negative increment", 0, [thm])
   else if i = 0 then thm
   else
-    Thm (deriv_rule1 (Proofterm.incr_indexes i) der,
+    Thm (deriv_rule1 (Proofterm.incr_indexes i, ZTerm.todo_proof) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx + i,
@@ -1944,7 +1970,8 @@
           raise CONTEXT (msg, [], [], [state], Option.map Context.Proof opt_ctxt);
       in
         Thm (deriv_rule1
-          (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der,
+          (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env,
+            ZTerm.todo_proof) der,
          {tags = [],
           maxidx = Envir.maxidx_of env,
           constraints = insert_constraints_env thy' env constraints,
@@ -1979,7 +2006,7 @@
     (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
       ~1 => raise THM ("eq_assumption", 0, [state])
     | n =>
-        Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,
+        Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1), ZTerm.todo_proof) der,
          {cert = cert,
           tags = [],
           maxidx = maxidx,
@@ -2009,7 +2036,7 @@
         in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
       else raise THM ("rotate_rule", k, [state]);
   in
-    Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m) der,
+    Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m, ZTerm.todo_proof) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -2043,7 +2070,7 @@
         in (prems', Logic.list_implies (prems', concl)) end
       else raise THM ("permute_prems: k", k, [rl]);
   in
-    Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m) der,
+    Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m, ZTerm.todo_proof) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -2201,7 +2228,8 @@
              Thm (deriv_rule2
                    (if Envir.is_empty env then bicompose_proof
                     else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env
-                    else Proofterm.norm_proof' env oo bicompose_proof) rder' sder,
+                    else Proofterm.norm_proof' env oo bicompose_proof,
+                    K ZTerm.todo_proof) rder' sder,
                 {tags = [],
                  maxidx = Envir.maxidx_of env,
                  constraints = constraints',
@@ -2220,7 +2248,7 @@
          else
            let val rename = rename_bvars dpairs tpairs B As0
            in (map (rename strip_apply) As0,
-             deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder)
+             deriv_rule1 (Proofterm.map_proof_terms (rename K) I, ZTerm.todo_proof) rder)
            end;
        in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
           handle TERM _ =>
diff -r ff68cbfa3550 -r 0c7de2ae814b src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Fri Dec 01 21:59:27 2023 +0100
+++ b/src/Pure/zterm.ML	Sat Dec 02 20:21:56 2023 +0100
@@ -38,11 +38,6 @@
   | ZAppP of zproof * zproof
   | ZClassP of ztyp * class        (*OFCLASS proof from sorts algebra*)
   | ZOracle of serial * zterm * ztyp list
-and zproof_body = ZPBody of
-  {boxes: (zterm * zproof future) Inttab.table,
-   consts: serial Ord_List.T,
-   oracles: ((string * Position.T) * zterm option) Ord_List.T,
-   proof: zproof}
 
 
 signature ZTERM =
@@ -56,6 +51,8 @@
   val typ_of: ztyp -> typ
   val zterm_of: Consts.T -> term -> zterm
   val term_of: Consts.T -> zterm -> term
+  val dummy_proof: 'a -> zproof
+  val todo_proof: 'a -> zproof
 end;
 
 structure ZTerm: ZTERM =
@@ -168,4 +165,10 @@
       | term (ZClass (T, c)) = Logic.mk_of_class (typ_of T, c);
   in term end;
 
+
+(* proofs *)
+
+fun dummy_proof _ = ZDummy;
+val todo_proof = dummy_proof;
+
 end;