src/Pure/term.ML
changeset 21682 53c9a026fcb7
parent 21493 47050cdc1694
child 21742 a330e58226d0
     1.1 --- a/src/Pure/term.ML	Wed Dec 06 21:18:58 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Wed Dec 06 21:18:59 2006 +0100
     1.3 @@ -156,10 +156,11 @@
     1.4    val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
     1.5    val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
     1.6    val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
     1.7 +  val add_varnames: term -> indexname list -> indexname list
     1.8    val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
     1.9    val add_tfrees: term -> (string * sort) list -> (string * sort) list
    1.10    val add_frees: term -> (string * typ) list -> (string * typ) list
    1.11 -  val add_varnames: term -> indexname list -> indexname list
    1.12 +  val hidden_polymorphism: term -> typ -> (indexname * sort) list
    1.13    val strip_abs_eta: int -> term -> (string * typ) list * term
    1.14    val fast_indexname_ord: indexname * indexname -> order
    1.15    val indexname_ord: indexname * indexname -> order
    1.16 @@ -486,6 +487,14 @@
    1.17  val add_tfrees = fold_types add_tfreesT;
    1.18  val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
    1.19  
    1.20 +(*extra type variables in a term, not covered by the type*)
    1.21 +fun hidden_polymorphism t T =
    1.22 +  let
    1.23 +    val tvarsT = add_tvarsT T [];
    1.24 +    val extra_tvars = fold_types (fold_atyps
    1.25 +      (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
    1.26 +  in extra_tvars end;
    1.27 +
    1.28  
    1.29  (** Comparing terms, types, sorts etc. **)
    1.30