src/Pure/type.ML
changeset 21116 be58cded79da
parent 20951 868120282837
child 21858 05f57309170c
     1.1 --- a/src/Pure/type.ML	Tue Oct 31 09:29:01 2006 +0100
     1.2 +++ b/src/Pure/type.ML	Tue Oct 31 09:29:06 2006 +0100
     1.3 @@ -40,7 +40,7 @@
     1.4    (*special treatment of type vars*)
     1.5    val strip_sorts: typ -> typ
     1.6    val no_tvars: typ -> typ
     1.7 -  val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
     1.8 +  val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
     1.9    val freeze_thaw_type: typ -> typ * (typ -> typ)
    1.10    val freeze_type: typ -> typ
    1.11    val freeze_thaw: term -> term * (term -> term)
    1.12 @@ -228,7 +228,7 @@
    1.13  
    1.14  (* varify *)
    1.15  
    1.16 -fun varify (t, fixed) =
    1.17 +fun varify fixed t =
    1.18    let
    1.19      val fs = Term.fold_types (Term.fold_atyps
    1.20        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    1.21 @@ -238,7 +238,7 @@
    1.22        (case AList.lookup (op =) fmap f of
    1.23          NONE => TFree f
    1.24        | SOME xi => TVar (xi, S));
    1.25 -  in (map_types (map_type_tfree thaw) t, fmap) end;
    1.26 +  in (fmap, map_types (map_type_tfree thaw) t) end;
    1.27  
    1.28  
    1.29  (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)