# HG changeset patch
# User wenzelm
# Date 1192547173 -7200
# Node ID 0dc445970b4be7b78aff020a47f9669352ae115e
# Parent  ec0547a4fcf039ffb47bdb3ca8b1a4a912dca851
tuned hidden_polymorphism;
added close_schematic_term;

diff -r ec0547a4fcf0 -r 0dc445970b4b src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Oct 16 17:06:11 2007 +0200
+++ b/src/Pure/term.ML	Tue Oct 16 17:06:13 2007 +0200
@@ -161,7 +161,7 @@
   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   val add_frees: term -> (string * typ) list -> (string * typ) list
-  val hidden_polymorphism: term -> typ -> (indexname * sort) list
+  val hidden_polymorphism: term -> (indexname * sort) list
   val strip_abs_eta: int -> term -> (string * typ) list * term
   val fast_indexname_ord: indexname * indexname -> order
   val indexname_ord: indexname * indexname -> order
@@ -179,6 +179,7 @@
   val eq_var: (indexname * typ) * (indexname * typ) -> bool
   val tvar_ord: (indexname * sort) * (indexname * sort) -> order
   val var_ord: (indexname * typ) * (indexname * typ) -> order
+  val close_schematic_term: term -> term
   val maxidx_typ: typ -> int -> int
   val maxidx_typs: typ list -> int -> int
   val maxidx_term: term -> int -> int
@@ -513,15 +514,17 @@
 val add_tfrees = fold_types add_tfreesT;
 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
 
-(*extra type variables in a term, not covered by the type*)
-fun hidden_polymorphism t T =
+(*extra type variables in a term, not covered by its type*)
+fun hidden_polymorphism t =
   let
+    val T = fastype_of t;
     val tvarsT = add_tvarsT T [];
     val extra_tvars = fold_types (fold_atyps
       (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   in extra_tvars end;
 
 
+
 (** Comparing terms, types, sorts etc. **)
 
 (* alpha equivalence -- tuned for equalities *)
@@ -1003,6 +1006,13 @@
           | subst (t $ u) = subst t $ subst u;
       in subst tm end;
 
+fun close_schematic_term t =
+  let
+    val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
+    val extra_terms = map Var (rev (add_vars t []));
+  in fold_rev lambda (extra_types @ extra_terms) t end;
+
+
 
 (** Identifying first-order terms **)