# HG changeset patch
# User wenzelm
# Date 1165436339 -3600
# Node ID 53c9a026fcb715c55e9af77e65d3e166a3cdb8cf
# Parent  8b8edcdb4da84cbd8427de8feb15633644ecb83f
added hidden_polymorphism (from variable.ML);

diff -r 8b8edcdb4da8 -r 53c9a026fcb7 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Dec 06 21:18:58 2006 +0100
+++ b/src/Pure/term.ML	Wed Dec 06 21:18:59 2006 +0100
@@ -156,10 +156,11 @@
   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
+  val add_varnames: term -> indexname list -> indexname list
   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 add_varnames: term -> indexname list -> indexname list
+  val hidden_polymorphism: term -> typ -> (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
@@ -486,6 +487,14 @@
 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 =
+  let
+    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. **)