# HG changeset patch
# User wenzelm
# Date 1628108447 -7200
# Node ID bc03b0b82fe6044679baa4a82997e390ecdd3650
# Parent  21ddf56ac1409fc59196c799fa60fd85573b7de6
prefer persistent hash code for cachable items (see also 72b13af7f266);

diff -r 21ddf56ac140 -r bc03b0b82fe6 src/Pure/term.scala
--- a/src/Pure/term.scala	Wed Aug 04 21:49:17 2021 +0200
+++ b/src/Pure/term.scala	Wed Aug 04 22:20:47 2021 +0200
@@ -15,6 +15,9 @@
 
   sealed case class Indexname(name: String, index: Int = 0)
   {
+    private lazy val hash: Int = (name, index).hashCode()
+    override def hashCode(): Int = hash
+
     override def toString: String =
       if (index == -1) name
       else {
@@ -36,17 +39,26 @@
   sealed abstract class Typ
   case class Type(name: String, args: List[Typ] = Nil) extends Typ
   {
+    private lazy val hash: Int = ("Type", name, args).hashCode()
+    override def hashCode(): Int = hash
+
     override def toString: String =
       if (this == dummyT) "_"
       else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")"
   }
   case class TFree(name: String, sort: Sort = Nil) extends Typ
   {
+    private lazy val hash: Int = ("TFree", name, sort).hashCode()
+    override def hashCode(): Int = hash
+
     override def toString: String =
       "TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
   }
   case class TVar(name: Indexname, sort: Sort = Nil) extends Typ
   {
+    private lazy val hash: Int = ("TVar", name, sort).hashCode()
+    override def hashCode(): Int = hash
+
     override def toString: String =
       "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
   }
@@ -62,24 +74,40 @@
   }
   case class Const(name: String, typargs: List[Typ] = Nil) extends Term
   {
+    private lazy val hash: Int = ("Const", name, typargs).hashCode()
+    override def hashCode(): Int = hash
+
     override def toString: String =
       if (this == dummy) "_"
       else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"
   }
   case class Free(name: String, typ: Typ = dummyT) extends Term
   {
+    private lazy val hash: Int = ("Free", name, typ).hashCode()
+    override def hashCode(): Int = hash
+
     override def toString: String =
       "Free(" + name + (if (typ == dummyT) "" else "," + typ) + ")"
   }
   case class Var(name: Indexname, typ: Typ = dummyT) extends Term
   {
+    private lazy val hash: Int = ("Var", name, typ).hashCode()
+    override def hashCode(): Int = hash
+
     override def toString: String =
       "Var(" + name + (if (typ == dummyT) "" else "," + typ) + ")"
   }
   case class Bound(index: Int) extends Term
   case class Abs(name: String, typ: Typ, body: Term) extends Term
+  {
+    private lazy val hash: Int = ("Abs", name, typ, body).hashCode()
+    override def hashCode(): Int = hash
+  }
   case class App(fun: Term, arg: Term) extends Term
   {
+    private lazy val hash: Int = ("App", fun, arg).hashCode()
+    override def hashCode(): Int = hash
+
     override def toString: String =
       this match {
         case OFCLASS(ty, c) => "OFCLASS(" + ty + "," + c + ")"
@@ -94,14 +122,50 @@
   case object MinProof extends Proof
   case class PBound(index: Int) extends Proof
   case class Abst(name: String, typ: Typ, body: Proof) extends Proof
+  {
+    private lazy val hash: Int = ("Abst", name, typ, body).hashCode()
+    override def hashCode(): Int = hash
+  }
   case class AbsP(name: String, hyp: Term, body: Proof) extends Proof
+  {
+    private lazy val hash: Int = ("AbsP", name, hyp, body).hashCode()
+    override def hashCode(): Int = hash
+  }
   case class Appt(fun: Proof, arg: Term) extends Proof
+  {
+    private lazy val hash: Int = ("Appt", fun, arg).hashCode()
+    override def hashCode(): Int = hash
+  }
   case class AppP(fun: Proof, arg: Proof) extends Proof
+  {
+    private lazy val hash: Int = ("AppP", fun, arg).hashCode()
+    override def hashCode(): Int = hash
+  }
   case class Hyp(hyp: Term) extends Proof
+  {
+    private lazy val hash: Int = ("Hyp", hyp).hashCode()
+    override def hashCode(): Int = hash
+  }
   case class PAxm(name: String, types: List[Typ]) extends Proof
+  {
+    private lazy val hash: Int = ("PAxm", name, types).hashCode()
+    override def hashCode(): Int = hash
+  }
   case class PClass(typ: Typ, cls: Class) extends Proof
+  {
+    private lazy val hash: Int = ("PClass", typ, cls).hashCode()
+    override def hashCode(): Int = hash
+  }
   case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
+  {
+    private lazy val hash: Int = ("Oracle", name, prop, types).hashCode()
+    override def hashCode(): Int = hash
+  }
   case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof
+  {
+    private lazy val hash: Int = ("PThm", serial, theory_name, name, types).hashCode()
+    override def hashCode(): Int = hash
+  }
 
 
   /* type classes within the logic */