diff -r bb9a3be6952a -r f0899dad4877 src/Pure/term.scala
--- a/src/Pure/term.scala	Thu May 24 16:56:14 2018 +0200
+++ b/src/Pure/term.scala	Thu May 24 21:13:09 2018 +0200
@@ -29,5 +29,63 @@
   case class Bound(index: Int) extends Term
   case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
   case class App(fun: Term, arg: Term) extends Term
+
+
+
+  /** cache **/
+
+  def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
+    new Cache(initial_size, max_string)
+
+  class Cache private[Term](initial_size: Int, max_string: Int)
+    extends isabelle.Cache(initial_size, max_string)
+  {
+    protected def cache_indexname(x: Indexname): Indexname =
+      lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
+
+    protected def cache_sort(x: Sort): Sort =
+      if (x == dummyS) dummyS
+      else lookup(x) getOrElse store(x.map(cache_string(_)))
+
+    protected def cache_typ(x: Typ): Typ =
+    {
+      if (x == dummyT) dummyT
+      else
+        lookup(x) match {
+          case Some(y) => y
+          case None =>
+            x match {
+              case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
+              case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
+              case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
+            }
+        }
+    }
+
+    protected def cache_term(x: Term): Term =
+    {
+      lookup(x) match {
+        case Some(y) => y
+        case None =>
+          x match {
+            case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
+            case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
+            case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
+            case Bound(index) => store(Bound(cache_int(index)))
+            case Abs(name, typ, body) =>
+              store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
+            case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
+          }
+      }
+    }
+
+    // main methods
+    def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
+    def sort(x: Sort): Sort = synchronized { cache_sort(x) }
+    def typ(x: Typ): Typ = synchronized { cache_typ(x) }
+    def term(x: Term): Term = synchronized { cache_term(x) }
+
+    def position(x: Position.T): Position.T =
+      synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
+  }
 }
-