# HG changeset patch
# User wenzelm
# Date 1570911507 -7200
# Node ID 6d01eca49b34ed82aa3f50d0167a3e6b3ce7babd
# Parent  006214c581ee11cfbb339a58109cc6cfcad119c2
clarified signature default;

diff -r 006214c581ee -r 6d01eca49b34 src/Pure/term.scala
--- a/src/Pure/term.scala	Sat Oct 12 22:12:29 2019 +0200
+++ b/src/Pure/term.scala	Sat Oct 12 22:18:27 2019 +0200
@@ -32,7 +32,6 @@
 
   type Class = String
   type Sort = List[Class]
-  val dummyS: Sort = List("")
 
   sealed abstract class Typ
   case class Type(name: String, args: List[Typ] = Nil) extends Typ
@@ -41,15 +40,15 @@
       if (this == dummyT) "_"
       else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")"
   }
-  case class TFree(name: String, sort: Sort = dummyS) extends Typ
+  case class TFree(name: String, sort: Sort = Nil) extends Typ
   {
     override def toString: String =
-      "TFree(" + name + (if (sort == dummyS) "" else "," + sort) + ")"
+      "TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
   }
-  case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ
+  case class TVar(name: Indexname, sort: Sort = Nil) extends Typ
   {
     override def toString: String =
-      "TVar(" + name + (if (sort == dummyS) "" else "," + sort) + ")"
+      "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
   }
   val dummyT = Type("dummy")
 
@@ -134,8 +133,7 @@
       lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
 
     protected def cache_sort(x: Sort): Sort =
-      if (x == dummyS) dummyS
-      else lookup(x) getOrElse store(x.map(cache_string(_)))
+      if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string(_)))
 
     protected def cache_typ(x: Typ): Typ =
     {