src/Pure/General/cache.scala

     }
   }
 
   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
     }
   }
 
   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"
     else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
     else {