disable thy_cache for now (amending 0b8922e351a3): avoid crash of AFP/Ramsey-Infinite due to exception THEORY "Duplicate theory name"; default tip
authorwenzelm
Tue, 23 Jul 2024 22:50:59 +0200
changeset 80613 42408be39d6c
parent 80612 e65eed943bee
disable thy_cache for now (amending 0b8922e351a3): avoid crash of AFP/Ramsey-Infinite due to exception THEORY "Duplicate theory name";
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;