# HG changeset patch
# User wenzelm
# Date 1165436340 -3600
# Node ID b90fa6c8e062d3c0e92c6eebcac328ee7caa372c
# Parent  53c9a026fcb715c55e9af77e65d3e166a3cdb8cf
moved hidden_polymorphism to term.ML;

diff -r 53c9a026fcb7 -r b90fa6c8e062 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Dec 06 21:18:59 2006 +0100
+++ b/src/Pure/variable.ML	Wed Dec 06 21:19:00 2006 +0100
@@ -28,7 +28,6 @@
   val declare_thm: thm -> Proof.context -> Proof.context
   val thm_context: thm -> Proof.context
   val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
-  val hidden_polymorphism: term -> typ -> (indexname * sort) list
   val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
   val expand_binds: Proof.context -> term -> term
   val add_fixes: string list -> Proof.context -> string list * Proof.context
@@ -223,19 +222,12 @@
 
 (** term bindings **)
 
-fun hidden_polymorphism t T =
-  let
-    val tvarsT = Term.add_tvarsT T [];
-    val extra_tvars = Term.fold_types (Term.fold_atyps
-      (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
-  in extra_tvars end;
-
 fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
   | add_bind ((x, i), SOME t) =
       let
         val T = Term.fastype_of t;
         val t' =
-          if null (hidden_polymorphism t T) then t
+          if null (Term.hidden_polymorphism t T) then t
           else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
       in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end;