src/Pure/thm.ML

--- a/src/Pure/thm.ML	Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/thm.ML	Thu Dec 14 17:33:45 2023 +0100
@@ -750,7 +750,7 @@
   make_deriv0 promises
     (PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof});
 
-val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes ZDummy MinProof;
+val empty_deriv = make_deriv [] [] [] ZTerm.empty_zboxes ZDummy MinProof;
 
 
 (* inference rules *)
@@ -768,7 +768,7 @@
 
     val oracles' = Proofterm.union_oracles oracles1 oracles2;
     val thms' = Proofterm.union_thms thms1 thms2;
-    val zboxes' = Proofterm.union_zboxes zboxes1 zboxes2;
+    val zboxes' = ZTerm.union_zboxes zboxes1 zboxes2;
 
     val proofs = Proofterm.get_proofs_level ();
     val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZDummy;
@@ -780,7 +780,7 @@
 fun deriv_rule0 zproof proof =
   let val proofs = Proofterm.get_proofs_level () in
     if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
-      deriv_rule1 I I (make_deriv [] [] [] Proofterm.empty_zboxes
+      deriv_rule1 I I (make_deriv [] [] [] ZTerm.empty_zboxes
        (if Proofterm.zproof_enabled proofs then zproof () else ZDummy)
        (if Proofterm.proof_enabled proofs then proof () else MinProof))
     else empty_deriv
@@ -844,7 +844,7 @@
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in
-    Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes ZDummy MinProof,
+    Thm (make_deriv [(i, future)] [] [] ZTerm.empty_zboxes ZDummy MinProof,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -985,12 +985,12 @@
 
 local
 
-val empty_digest = ([], [], Proofterm.empty_zboxes);
+val empty_digest = ([], [], ZTerm.empty_zboxes);
 
 fun union_digest (oracles1, thms1, zboxes1) (oracles2, thms2, zboxes2) =
  (Proofterm.union_oracles oracles1 oracles2,
   Proofterm.union_thms thms1 thms2,
-  Proofterm.union_zboxes zboxes1 zboxes2);
+  ZTerm.union_zboxes zboxes1 zboxes2);
 
 fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, zboxes, ...}, ...}, _)) =
   (oracles, thms, zboxes);
@@ -1171,7 +1171,7 @@
               then ZTerm.oracle_proof (Context.certificate_theory cert) name prop
               else ZDummy;
           in
-            Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes zproof proof,
+            Thm (make_deriv [] [oracle] [] ZTerm.empty_zboxes zproof proof,
              {cert = cert,
               tags = [],
               maxidx = maxidx,