# 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;