# HG changeset patch
# User wenzelm
# Date 1563616110 -7200
# Node ID 38ac2e714729b1b0a456874d76e76372e85c955a
# Parent  23ba5a638e6d850b27e67e3e89cb06a59932e74a
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);

diff -r 23ba5a638e6d -r 38ac2e714729 src/Pure/term.scala
--- a/src/Pure/term.scala	Sat Jul 20 11:17:54 2019 +0200
+++ b/src/Pure/term.scala	Sat Jul 20 11:48:30 2019 +0200
@@ -11,6 +11,8 @@
 
 object Term
 {
+  /* types and terms */
+
   type Indexname = (String, Int)
 
   type Sort = List[String]
@@ -31,6 +33,32 @@
   case class App(fun: Term, arg: Term) extends Term
 
 
+  /* 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 **/