src/Pure/General/cache.scala

--- a/src/Pure/General/cache.scala	Sat Jan 02 16:09:45 2021 +0100
+++ b/src/Pure/General/cache.scala	Sat Jan 02 16:12:52 2021 +0100
@@ -45,7 +45,7 @@
 
   protected def store[A](x: A): A =
   {
-    if (table == null) x
+    if (table == null || x == null) x
     else {
       table.put(x, new WeakReference[Any](x))
       x
@@ -54,7 +54,8 @@
 
   protected def cache_string(x: String): String =
   {
-    if (x == "") ""
+    if (x == null) null
+    else if (x == "") ""
     else if (x == "true") "true"
     else if (x == "false") "false"
     else if (x == "0.0") "0.0"