# HG changeset patch
# User wenzelm
# Date 1570199654 -7200
# Node ID d50c8f4f209050f0eb3826df4008b5d0f01b58c3
# Parent  edaeb8feb4d069619769456d4ec6461b2ef7a861
obsolete;

diff -r edaeb8feb4d0 -r d50c8f4f2090 src/Pure/term.scala
--- a/src/Pure/term.scala	Fri Oct 04 16:25:45 2019 +0200
+++ b/src/Pure/term.scala	Fri Oct 04 16:34:14 2019 +0200
@@ -64,10 +64,6 @@
 
   /* Pure logic */
 
-  def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty))
-  val propT: Typ = Type(Pure_Thy.PROP, Nil)
-  def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2))
-
   def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, List(ty))
 
   def const_of_class(c: String): String = c + "_class"
@@ -79,32 +75,6 @@
   }
 
 
-  /* type arguments of consts */
-
-  def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] =
-  {
-    var subst = Map.empty[String, Typ]
-
-    def bad_match(): Nothing = error("Malformed type instance for " + name + ": " + typ)
-    def raw_match(arg: (Typ, Typ))
-    {
-      arg match {
-        case (TFree(a, _), ty) =>
-          subst.get(a) match {
-            case None => subst += (a -> ty)
-            case Some(ty1) => if (ty != ty1) bad_match()
-          }
-        case (Type(c1, args1), Type(c2, args2)) if c1 == c2 =>
-          (args1 zip args2).foreach(raw_match)
-        case _ => bad_match()
-      }
-    }
-    raw_match(decl, typ)
-
-    typargs.map(subst)
-  }
-
-
 
   /** cache **/