--- a/src/Pure/General/table.ML Mon Jun 03 20:56:21 2024 +0100
+++ b/src/Pure/General/table.ML Mon Jun 03 20:56:41 2024 +0100
@@ -592,15 +592,20 @@
(* cache *)
fun unsynchronized_cache f =
- let val cache = Unsynchronized.ref empty in
+ let
+ val cache1 = Unsynchronized.ref empty;
+ val cache2 = Unsynchronized.ref empty;
+ in
fn x =>
- (case lookup (! cache) x of
- SOME result => Exn.release result
+ (case lookup (! cache1) x of
+ SOME y => y
| NONE =>
- let
- val result = Exn.result f x;
- val _ = Unsynchronized.change cache (update (x, result));
- in Exn.release result end)
+ (case lookup (! cache2) x of
+ SOME exn => Exn.reraise exn
+ | NONE =>
+ (case Exn.result f x of
+ Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y)
+ | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))))
end;
--- a/src/Pure/proofterm.ML Mon Jun 03 20:56:21 2024 +0100
+++ b/src/Pure/proofterm.ML Mon Jun 03 20:56:41 2024 +0100
@@ -100,7 +100,6 @@
val fold_proof_terms: (term -> 'a -> 'a) -> proof -> 'a -> 'a
val fold_proof_terms_types: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
val maxidx_proof: proof -> int -> int
- val size_of_proof: proof -> int
val change_types: typ list option -> proof -> proof
val abstract_over: term -> proof -> proof
val incr_bv_same: int -> int -> int -> int -> proof Same.operation
@@ -595,12 +594,6 @@
fun maxidx_proof prf = fold_proof_terms_types Term.maxidx_term Term.maxidx_typ prf;
-fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf
- | size_of_proof (AbsP (_, _, prf)) = 1 + size_of_proof prf
- | size_of_proof (prf % _) = 1 + size_of_proof prf
- | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2
- | size_of_proof _ = 1;
-
fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
| change_types (SOME [T]) (PClass (_, c)) = PClass (T, c)
| change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)