# HG changeset patch
# User wenzelm
# Date 1721767859 -7200
# Node ID 42408be39d6c95fe688c15e0272d9ca5b0ae53df
# Parent  e65eed943bee9057f88d021a7a30669293f007ad
disable thy_cache for now (amending 0b8922e351a3): avoid crash of AFP/Ramsey-Infinite due to exception THEORY "Duplicate theory name";

diff -r e65eed943bee -r 42408be39d6c src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Tue Jul 23 15:54:43 2024 +0100
+++ b/src/Pure/Build/export_theory.ML	Tue Jul 23 22:50:59 2024 +0200
@@ -140,7 +140,7 @@
 
     (* recode *)
 
-    val thy_cache = perhaps ZTerm.init_cache thy;
+    val thy_cache = thy;  (* FIXME tmp *)
 
     val ztyp_of = ZTerm.ztyp_cache thy_cache;
     val zterm_of = ZTerm.zterm_of thy_cache;