--- 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 **)