fixed type signature of Type.varify

--- a/src/HOL/Tools/old_inductive_package.ML	Tue Oct 31 09:29:01 2006 +0100
+++ b/src/HOL/Tools/old_inductive_package.ML	Tue Oct 31 09:29:06 2006 +0100
@@ -173,14 +173,14 @@
   (let
     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     fun varify (t, (i, ts)) =
-      let val t' = map_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
+      let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
       in (maxidx_of_term t', t'::ts) end;
     val (i, cs') = foldr varify (~1, []) cs;
     val (i', intr_ts') = foldr varify (i, []) intr_ts;
     val rec_consts = fold add_term_consts_2 cs' [];
     val intr_consts = fold add_term_consts_2 intr_ts' [];
     fun unify (cname, cT) =
-      let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
+      let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
     val (env, _) = fold unify rec_consts (Vartab.empty, i');
     val subst = Type.freeze o map_types (Envir.norm_type env)

--- a/src/HOL/Tools/specification_package.ML	Tue Oct 31 09:29:01 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Tue Oct 31 09:29:06 2006 +0100
@@ -140,7 +140,7 @@
         val prop  = myfoldr HOLogic.mk_conj (map fst props'')
         val cprop = cterm_of thy (HOLogic.mk_Trueprop prop)
 
-        val (prop_thawed,vmap) = Type.varify (prop,[])
+        val (vmap, prop_thawed) = Type.varify [] prop
         val thawed_prop_consts = collect_consts (prop_thawed,[])
         val (altcos,overloaded) = Library.split_list cos
         val (names,sconsts) = Library.split_list altcos
@@ -150,7 +150,7 @@
 
         fun proc_const c =
             let
-                val c' = fst (Type.varify (c,[]))
+                val (_, c') = Type.varify [] c
                 val (cname,ctyp) = dest_Const c'
             in
                 case List.filter (fn t => let val (name,typ) = dest_Const t

--- a/src/Pure/Proof/reconstruct.ML	Tue Oct 31 09:29:01 2006 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Tue Oct 31 09:29:06 2006 +0100
@@ -144,7 +144,7 @@
           let
             val tvars = term_tvars prop;
             val tfrees = term_tfrees prop;
-            val (prop', fmap) = Type.varify (prop, []);
+            val (fmap, prop') = Type.varify [] prop;
             val (env', Ts) = (case opTs of
                 NONE => foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
               | SOME Ts => (env, Ts));
@@ -306,7 +306,7 @@
   end;
 
 fun prop_of_atom prop Ts =
-  let val (prop', fmap) = Type.varify (prop, []);
+  let val (fmap, prop') = Type.varify [] prop;
   in subst_TVars (map fst (term_tvars prop) @ map snd fmap ~~ Ts)
     (forall_intr_vfs prop')
   end;

--- a/src/Pure/thm.ML	Tue Oct 31 09:29:01 2006 +0100
+++ b/src/Pure/thm.ML	Tue Oct 31 09:29:06 2006 +0100
@@ -1176,7 +1176,7 @@
   let
     val tfrees = foldr add_term_tfrees fixed hyps;
     val prop1 = attach_tpairs tpairs prop;
-    val (prop2, al) = Type.varify (prop1, tfrees);
+    val (al, prop2) = Type.varify tfrees prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
     (al, Thm {thy_ref = thy_ref,

--- a/src/Pure/type.ML	Tue Oct 31 09:29:01 2006 +0100
+++ b/src/Pure/type.ML	Tue Oct 31 09:29:06 2006 +0100
@@ -40,7 +40,7 @@
   (*special treatment of type vars*)
   val strip_sorts: typ -> typ
   val no_tvars: typ -> typ
-  val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
+  val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
   val freeze_thaw_type: typ -> typ * (typ -> typ)
   val freeze_type: typ -> typ
   val freeze_thaw: term -> term * (term -> term)
@@ -228,7 +228,7 @@
 
 (* varify *)
 
-fun varify (t, fixed) =
+fun varify fixed t =
   let
     val fs = Term.fold_types (Term.fold_atyps
       (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
@@ -238,7 +238,7 @@
       (case AList.lookup (op =) fmap f of
         NONE => TFree f
       | SOME xi => TVar (xi, S));
-  in (map_types (map_type_tfree thaw) t, fmap) end;
+  in (fmap, map_types (map_type_tfree thaw) t) end;
 
 
 (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)