diff -r 2acdaa0a7d29 -r 446b887e23c7 src/Pure/term.scala
--- a/src/Pure/term.scala	Sun Jul 14 16:17:31 2024 +0200
+++ b/src/Pure/term.scala	Sun Jul 14 17:49:30 2024 +0200
@@ -96,17 +96,17 @@
   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 + ")"
-        case _ => "App(" + fun + "," + arg + ")"
-      }
+  }
+  case class OFCLASS(typ: Typ, name: String) extends Term {
+    private lazy val hash: Int = ("OFCLASS", typ, name).hashCode()
+    override def hashCode(): Int = hash
   }
 
   def dummy_pattern(ty: Typ): Term = Const("Pure.dummy_pattern", List(ty))
   val dummy: Term = dummy_pattern(dummyT)
 
+  def mk_of_sort(typ: Typ, s: Sort): List[Term] = s.map(c => OFCLASS(typ, c))
+
   sealed abstract class Proof
   case object MinProof extends Proof
   case class PBound(index: Int) extends Proof
@@ -148,30 +148,6 @@
   }
 
 
-  /* type classes within the logic */
-
-  object Class_Const {
-    val suffix = "_class"
-    def apply(c: Class): String = c + suffix
-    def unapply(s: String): Option[Class] =
-      if (s.endsWith(suffix)) Some(s.substring(0, s.length - suffix.length)) else None
-  }
-
-  object OFCLASS {
-    def apply(ty: Typ, s: Sort): List[Term] = s.map(c => apply(ty, c))
-
-    def apply(ty: Typ, c: Class): Term =
-      App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty)))
-
-    def unapply(t: Term): Option[(Typ, String)] =
-      t match {
-        case App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty1)))
-        if ty == ty1 => Some((ty, c))
-        case _ => None
-      }
-  }
-
-
 
   /** cache **/
 
@@ -230,6 +206,7 @@
             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)))
+            case OFCLASS(typ, name) => store(OFCLASS(cache_typ(typ), cache_string(name)))
           }
       }
     }