src/Pure/type.ML
changeset 19305 5c16895d548b
parent 19250 932a50e2332f
child 19464 d13309e30aba
     1.1 --- a/src/Pure/type.ML	Tue Mar 21 12:18:13 2006 +0100
     1.2 +++ b/src/Pure/type.ML	Tue Mar 21 12:18:15 2006 +0100
     1.3 @@ -220,7 +220,8 @@
     1.4  
     1.5  fun varify (t, fixed) =
     1.6    let
     1.7 -    val fs = add_term_tfrees (t, []) \\ fixed;
     1.8 +    val fs = Term.fold_types (Term.fold_atyps
     1.9 +      (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    1.10      val ixns = add_term_tvar_ixns (t, []);
    1.11      val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
    1.12      fun thaw (f as (a, S)) =