# HG changeset patch
# User wenzelm
# Date 1594910892 -7200
# Node ID d3b8c8b2d1fc0c8eb14db023563c5f9ec0b7019c
# Parent  b9e9ff3a1e1c4630fa45d295d94701697d101f97
more thorough extend/merge (for Theory.join_theory);

diff -r b9e9ff3a1e1c -r d3b8c8b2d1fc src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Jul 16 16:38:25 2020 +0200
+++ b/src/Pure/more_thm.ML	Thu Jul 16 16:48:12 2020 +0200
@@ -654,16 +654,24 @@
 
 structure Proofs = Theory_Data
 (
-  type T = thm list lazy list;
-  val empty = [];
-  fun extend _ = empty;
-  fun merge _ = empty;
+  type T = thm list lazy Inttab.table;
+  val empty = Inttab.empty;
+  val extend = I;
+  val merge = Inttab.merge (K true);
 );
 
-fun register_proofs ths =
-  (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths);
+fun reset_proofs thy =
+  if Inttab.is_empty (Proofs.get thy) then NONE
+  else SOME (Proofs.put Inttab.empty thy);
+
+val _ = Theory.setup (Theory.at_begin reset_proofs);
 
-fun force_proofs thy = rev (Proofs.get thy) |> maps (map (Thm.transfer thy) o Lazy.force);
+fun register_proofs ths thy =
+  let val entry = (serial (), Lazy.map_finished (map Thm.trim_context) ths)
+  in (Proofs.map o Inttab.update) entry thy end;
+
+fun force_proofs thy =
+  Proofs.get thy |> Inttab.dest |> maps (map (Thm.transfer thy) o Lazy.force o #2);
 
 val consolidate_theory = Thm.consolidate o force_proofs;