moved hidden_polymorphism to term.ML;
authorwenzelm
Wed Dec 06 21:19:00 2006 +0100 (2006-12-06)
changeset 21683b90fa6c8e062
parent 21682 53c9a026fcb7
child 21684 e8c135b166b3
moved hidden_polymorphism to term.ML;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Wed Dec 06 21:18:59 2006 +0100
     1.2 +++ b/src/Pure/variable.ML	Wed Dec 06 21:19:00 2006 +0100
     1.3 @@ -28,7 +28,6 @@
     1.4    val declare_thm: thm -> Proof.context -> Proof.context
     1.5    val thm_context: thm -> Proof.context
     1.6    val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
     1.7 -  val hidden_polymorphism: term -> typ -> (indexname * sort) list
     1.8    val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
     1.9    val expand_binds: Proof.context -> term -> term
    1.10    val add_fixes: string list -> Proof.context -> string list * Proof.context
    1.11 @@ -223,19 +222,12 @@
    1.12  
    1.13  (** term bindings **)
    1.14  
    1.15 -fun hidden_polymorphism t T =
    1.16 -  let
    1.17 -    val tvarsT = Term.add_tvarsT T [];
    1.18 -    val extra_tvars = Term.fold_types (Term.fold_atyps
    1.19 -      (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
    1.20 -  in extra_tvars end;
    1.21 -
    1.22  fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
    1.23    | add_bind ((x, i), SOME t) =
    1.24        let
    1.25          val T = Term.fastype_of t;
    1.26          val t' =
    1.27 -          if null (hidden_polymorphism t T) then t
    1.28 +          if null (Term.hidden_polymorphism t T) then t
    1.29            else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
    1.30        in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end;
    1.31