src/Pure/thm.ML

--- a/src/Pure/thm.ML	Tue Apr 11 15:03:02 2023 +0200
+++ b/src/Pure/thm.ML	Tue Apr 11 20:32:04 2023 +0200
@@ -107,7 +107,7 @@
   val expose_proofs: theory -> thm list -> unit
   val expose_proof: theory -> thm -> unit
   val future: thm future -> cterm -> thm
-  val thm_deps: thm -> Proofterm.thm Ord_List.T
+  val thm_deps: thm -> Proofterm.thms
   val extra_shyps: thm -> Sortset.T
   val strip_shyps: thm -> thm
   val derivation_closed: thm -> bool
@@ -739,7 +739,7 @@
 fun make_deriv promises oracles thms proof =
   Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
 
-val empty_deriv = make_deriv empty_promises Oracles.empty [] MinProof;
+val empty_deriv = make_deriv empty_promises Oracles.empty PThms.empty MinProof;
 
 
 (* inference rules *)
@@ -753,7 +753,7 @@
   let
     val ps = merge_promises (promises1, promises2);
     val oracles = Oracles.merge (oracles1, oracles2);
-    val thms = Proofterm.unions_thms [thms1, thms2];
+    val thms = Proofterm.union_thms (thms1, thms2);
     val prf =
       (case ! Proofterm.proofs of
         2 => f prf1 prf2
@@ -766,7 +766,7 @@
 
 fun deriv_rule0 make_prf =
   if ! Proofterm.proofs <= 1 then empty_deriv
-  else deriv_rule1 I (make_deriv empty_promises Oracles.empty [] (make_prf ()));
+  else deriv_rule1 I (make_deriv empty_promises Oracles.empty PThms.empty (make_prf ()));
 
 fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
   make_deriv promises oracles thms (f proof);
@@ -832,7 +832,7 @@
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in
-    Thm (make_deriv (make_promises [(i, future)]) Oracles.empty [] MinProof,
+    Thm (make_deriv (make_promises [(i, future)]) Oracles.empty PThms.empty MinProof,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -974,7 +974,7 @@
 local
 
 fun union_digest (oracles1, thms1) (oracles2, thms2) =
-  (Oracles.merge (oracles1, oracles2), Proofterm.unions_thms [thms1, thms2]);
+  (Oracles.merge (oracles1, oracles2), Proofterm.union_thms (thms1, thms2));
 
 fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
   (oracles, thms);
@@ -982,11 +982,12 @@
 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 (Oracles.empty, []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
+      if c1 = c2 then (Oracles.empty, PThms.empty)
+      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 (Oracles.empty, [])) (Type.sort_of_atyp T)}
+    type_variable = fn T => map (pair (Oracles.empty, PThms.empty)) (Type.sort_of_atyp T)}
    (typ, sort);
 
 in
@@ -1093,12 +1094,13 @@
 
 (*dependencies of PThm node*)
 fun thm_deps (thm as Thm (Deriv {promises, body = PBody {thms, ...}, ...}, _)) =
-  if null_promises promises then
-      (case (derivation_id thm, thms) of
-        (SOME {serial = i, ...}, [(j, thm_node)]) =>
-          if i = j then Proofterm.thm_node_thms thm_node else thms
-      | _ => thms)
-  else raise THM ("thm_deps: bad promises", 0, [thm]);
+  if not (null_promises promises) then raise THM ("thm_deps: bad promises", 0, [thm])
+  else if PThms.size thms = 1 then
+    (case (derivation_id thm, PThms.dest thms) of
+      (SOME {serial = i, ...}, [(j, thm_node)]) =>
+        if i = j then Proofterm.thm_node_thms thm_node else thms
+    | _ => thms)
+  else thms;
 
 fun name_derivation name_pos =
   strip_shyps #> (fn thm as Thm (der, args) =>
@@ -1114,7 +1116,7 @@
       val (pthm, proof) =
         Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
           name_pos shyps (Termset.dest hyps) prop ps body;
-      val der' = make_deriv empty_promises Oracles.empty [pthm] proof;
+      val der' = make_deriv empty_promises Oracles.empty (PThms.make [pthm]) proof;
     in Thm (der', args) end);
 
 fun close_derivation pos =
@@ -1145,7 +1147,7 @@
               | 0 => (((name, Position.none), NONE), MinProof)
               | i => bad_proofs i);
           in
-            Thm (make_deriv empty_promises (Oracles.make [oracle]) [] prf,
+            Thm (make_deriv empty_promises (Oracles.make [oracle]) PThms.empty prf,
              {cert = Context.join_certificate (Context.Certificate thy', cert2),
               tags = [],
               maxidx = maxidx,
@@ -1805,7 +1807,7 @@
       val (pthm, proof) =
         Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
           shyps prop ps body;
-      val der' = make_deriv empty_promises Oracles.empty [pthm] proof;
+      val der' = make_deriv empty_promises Oracles.empty (PThms.make [pthm]) proof;
       val prop' = Proofterm.thm_node_prop (#2 pthm);
     in
       Thm (der',