--- a/src/Pure/General/cache.scala Wed Jun 06 14:18:25 2018 +0200
+++ b/src/Pure/General/cache.scala Wed Jun 06 14:18:31 2018 +0200
@@ -1,4 +1,4 @@
-/* Title: Pure/cache.scala
+/* Title: Pure/General/cache.scala
Author: Makarius
cache for partial sharing (weak table).