# HG changeset patch
# User wenzelm
# Date 1131975458 -3600
# Node ID 9b729737bf14497824fd2a1765efa0e8a6261a48
# Parent  1a6161e92b4959056cef004f5e84b22ca3f586dd
added instance;

diff -r 1a6161e92b49 -r 9b729737bf14 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Mon Nov 14 14:37:15 2005 +0100
+++ b/src/Pure/consts.ML	Mon Nov 14 14:37:38 2005 +0100
@@ -14,6 +14,7 @@
   val constraint: T -> string -> typ    (*exception TYPE*)
   val monomorphic: T -> string -> bool
   val typargs: T -> string * typ -> typ list
+  val instance: T -> string * typ list -> typ
   val declare: NameSpace.naming -> bstring * typ -> T -> T
   val constrain: string * typ -> T -> T
   val hide: bool -> string -> T -> T
@@ -68,6 +69,12 @@
 
 fun typargs consts (c, T) = map (sub T) (#2 (the_const consts c));
 
+fun instance consts (c, Ts) =
+  let
+    val declT = declaration consts c;
+    val vars = map Term.dest_TVar (typargs consts (c, declT));
+  in declT |> Term.instantiateT (vars ~~ Ts) end;
+
 
 
 (** build consts **)