renamed Type.(un)varifyT to Logic.(un)varifyT;
made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;

--- a/src/HOL/Library/word_setup.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/HOL/Library/word_setup.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -35,8 +35,8 @@
 		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
 		else NONE
 	      | g _ _ _ = NONE
-  (*lcp**	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***)
-	    val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g
+  (*lcp**	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f ***)
+	    val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
 	in
 	  Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]);
           thy

--- a/src/HOL/Tools/datatype_realizer.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -147,7 +147,7 @@
      (foldr (fn ((f, p), prf) =>
         (case head_of (strip_abs_body f) of
            Free (s, T) =>
-             let val T' = Type.varifyT T
+             let val T' = Logic.varifyT T
              in Abst (s, SOME T', Proofterm.prf_abstract_over
                (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
              end
@@ -164,8 +164,7 @@
 
 fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info, thy) =
   let
-    val sg = sign_of thy;
-    val cert = cterm_of sg;
+    val cert = cterm_of thy;
     val rT = TFree ("'P", HOLogic.typeS);
     val rT' = TVar (("'P", 0), HOLogic.typeS);
 
@@ -187,7 +186,7 @@
     val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
     val r = Const (case_name, map fastype_of rs ---> T --> rT);
 
-    val y = Var (("y", 0), Type.varifyT T);
+    val y = Var (("y", 0), Logic.legacy_varifyT T);
     val y' = Free ("y", T);
 
     val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
@@ -208,10 +207,10 @@
     val P = Var (("P", 0), rT' --> HOLogic.boolT);
     val prf = forall_intr_prf (y, forall_intr_prf (P,
       foldr (fn ((p, r), prf) =>
-        forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
+        forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p),
           prf))) (Proofterm.proof_combP (prf_of thm',
             map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
-    val r' = Logic.varify (Abs ("y", Type.varifyT T,
+    val r' = Logic.legacy_varify (Abs ("y", Logic.legacy_varifyT T,
       list_abs (map dest_Free rs, list_comb (r,
         map Bound ((length rs - 1 downto 0) @ [length rs])))));
 

--- a/src/HOL/Tools/function_package/termination.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -31,7 +31,7 @@
 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom =
     let
 	val domT = domain_type (fastype_of f)
-	val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
+	val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
 	val DT = type_of D
 	val idomT = HOLogic.dest_setT DT
 

--- a/src/HOL/Tools/inductive_realizer.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -60,9 +60,9 @@
     val params = map dest_Var ts;
     val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
     fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
-      map (Type.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
+      map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
         filter_out (equal Extraction.nullT) (map
-          (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
+          (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
             NoSyn);
   in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
     map constr_of_intr intrs)

--- a/src/Pure/IsaPlanner/term_lib.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -661,15 +661,15 @@
   fun change_vars_to_frees (a$b) =
         (change_vars_to_frees a) $ (change_vars_to_frees b)
     | change_vars_to_frees (Abs(s,ty,t)) =
-        (Abs(s,Type.varifyT ty,change_vars_to_frees t))
-    | change_vars_to_frees (Var((s,i),ty)) = (Free(s,Type.unvarifyT ty))
+        (Abs(s, Logic.legacy_varifyT ty,change_vars_to_frees t))
+    | change_vars_to_frees (Var((s,i),ty)) = (Free(s, Logic.legacy_unvarifyT ty))
     | change_vars_to_frees l = l;
 
   fun change_frees_to_vars (a$b) =
         (change_frees_to_vars a) $ (change_frees_to_vars b)
     | change_frees_to_vars (Abs(s,ty,t)) =
-        (Abs(s,Type.varifyT ty,change_frees_to_vars t))
-    | change_frees_to_vars (Free(s,ty)) = (Var((s,0),Type.varifyT ty))
+        (Abs(s, Logic.legacy_varifyT ty,change_frees_to_vars t))
+    | change_frees_to_vars (Free(s,ty)) = (Var((s,0), Logic.legacy_varifyT ty))
     | change_frees_to_vars l = l;
 
 

--- a/src/Pure/Tools/class_package.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -499,7 +499,7 @@
       in
         thy
         |> Sign.add_const_constraint_i (c, NONE)
-        |> pair (c, Type.unvarifyT ty)
+        |> pair (c, Logic.legacy_unvarifyT ty)
       end;
     fun check_defs0 thy raw_defs c_req =
       let
@@ -508,8 +508,8 @@
         val c_given = map get_c raw_defs;
         fun eq_c ((c1 : string, ty1), (c2, ty2)) =
           let
-            val ty1' = Type.varifyT ty1;
-            val ty2' = Type.varifyT ty2;
+            val ty1' = Logic.legacy_varifyT ty1;
+            val ty2' = Logic.legacy_varifyT ty2;
           in
             c1 = c2
             andalso Sign.typ_instance thy (ty1', ty2')
@@ -649,8 +649,8 @@
 
 fun extract_lookup thy sortctxt raw_typ_def raw_typ_use =
   let
-    val typ_def = Type.varifyT raw_typ_def;
-    val typ_use = Type.varifyT raw_typ_use;
+    val typ_def = Logic.legacy_varifyT raw_typ_def;
+    val typ_use = Logic.legacy_varifyT raw_typ_use;
     val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
     fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
     fun mk_class_deriv thy subclasses superclass =
@@ -682,14 +682,14 @@
 fun extract_classlookup thy (c, raw_typ_use) =
   let
     val raw_typ_def = Sign.the_const_constraint thy c;
-    val typ_def = Type.varifyT raw_typ_def;
+    val typ_def = Logic.legacy_varifyT raw_typ_def;
     fun reorder_sortctxt ctxt =
       case lookup_const_class thy c
        of NONE => ctxt
         | SOME class =>
             let
               val data = the_class_data thy class;
-              val sign = (Type.varifyT o the o AList.lookup (op =) ((map snd o #consts) data)) c;
+              val sign = (Logic.legacy_varifyT o the o AList.lookup (op =) ((map snd o #consts) data)) c;
               val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty;
               val v : string = case Vartab.lookup match_tab (#var data, 0)
                 of SOME (_, TVar ((v, _), _)) => v;

--- a/src/Pure/Tools/codegen_package.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -605,7 +605,7 @@
       |> fold_map (ensure_def_class thy tabs) clss
       |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i))))
 and mk_fun thy tabs (c, ty) trns =
-  case CodegenTheorems.get_funs thy (c, Type.varifyT ty)
+  case CodegenTheorems.get_funs thy (c, Logic.legacy_varifyT ty)  (* FIXME *)
    of SOME (ty, eq_thms) =>
         let
           val sortctxt = ClassPackage.extract_sortctxt thy ty;
@@ -849,7 +849,7 @@
 
 fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
   let
-    val ty_def = (op ---> o apfst tl o strip_type o Type.unvarifyT o Sign.the_const_type thy) c;
+    val ty_def = (op ---> o apfst tl o strip_type o Logic.legacy_unvarifyT o Sign.the_const_type thy) c;
     val ty' = (op ---> o apfst tl o strip_type) ty;
     val idf = idf_of_const thy tabs (c, ty);
   in

--- a/src/Pure/Tools/codegen_theorems.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -619,7 +619,7 @@
 
 fun preprocess_term thy raw_t =
   let
-    val t = (Term.map_term_types Type.varifyT o Logic.varify) raw_t;
+    val t = Logic.legacy_varify raw_t;
     val x = variant (add_term_names (t, [])) "a";
     val t_eq = Logic.mk_equals (Free (x, fastype_of t), t);
     (*fake definition*)

--- a/src/Pure/codegen.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/codegen.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -558,7 +558,7 @@
 (**** retrieve definition of constant ****)
 
 fun is_instance thy T1 T2 =
-  Sign.typ_instance thy (T1, Type.varifyT T2);
+  Sign.typ_instance thy (T1, Logic.legacy_varifyT T2);
 
 fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) =>
   s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));

--- a/src/Pure/defs.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/defs.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -33,7 +33,7 @@
   let
     val prt_args =
       if null args then []
-      else [Pretty.list "(" ")" (map (Pretty.typ pp o Type.freeze_type) args)];
+      else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT) args)];
   in Pretty.block (Pretty.str c :: prt_args) end;
 
 fun plain_args args =

--- a/src/Pure/display.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/display.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -169,7 +169,7 @@
     fun prt_sort S = Sign.pretty_sort thy S;
     fun prt_arity t (c, (_, Ss)) = Sign.pretty_arity thy (t, Ss, [c]);
     fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
-    val prt_typ_no_tvars = prt_typ o Type.freeze_type;
+    val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
     fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
     val prt_term_no_vars = prt_term o Logic.unvarify;
     fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];

--- a/src/Pure/logic.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/logic.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -67,8 +67,14 @@
   val set_rename_prefix: string -> unit
   val list_rename_params: string list * term -> term
   val assum_pairs: int * term -> (term*term)list
+  val varifyT: typ -> typ
+  val unvarifyT: typ -> typ
   val varify: term -> term
   val unvarify: term -> term
+  val legacy_varifyT: typ -> typ
+  val legacy_unvarifyT: typ -> typ
+  val legacy_varify: term -> term
+  val legacy_unvarify: term -> term
   val get_goal: term -> int -> term
   val goal_params: term -> int -> term * term list
   val prems_of_goal: term -> int -> term list
@@ -492,7 +498,7 @@
       all T $ Abs(c, T, list_rename_params (cs, t))
   | list_rename_params (cs, B) = B;
 
-(*** Treatmsent of "assume", "erule", etc. ***)
+(*** Treatment of "assume", "erule", etc. ***)
 
 (*Strips assumptions in goal yielding
    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
@@ -529,22 +535,46 @@
   in  pairrev (Hs,[])
   end;
 
-(*Converts Frees to Vars and TFrees to TVars*)
-fun varify (Const(a, T)) = Const (a, Type.varifyT T)
-  | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T)
-  | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T)
-  | varify (t as Bound _) = t
-  | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body)
-  | varify (f $ t) = varify f $ varify t;
+
+(* global schematic variables *)
+
+fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
+fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
+
+fun varifyT ty = ty |> Term.map_atyps
+  (fn TFree (a, S) => TVar ((a, 0), S)
+    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
+
+fun unvarifyT ty = ty |> Term.map_atyps
+  (fn TVar ((a, 0), S) => TFree (a, S)
+    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
+    | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
 
-(*Inverse of varify.*)
-fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T)
-  | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T)
-  | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)
-  | unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T)  (*non-0 index!*)
-  | unvarify (t as Bound _) = t
-  | unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body)
-  | unvarify (f $ t) = unvarify f $ unvarify t;
+fun varify tm =
+  tm |> Term.map_aterms
+    (fn Free (x, T) => Var ((x, 0), T)
+      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
+      | t => t)
+  |> Term.map_term_types varifyT;
+
+fun unvarify tm =
+  tm |> Term.map_aterms
+    (fn Var ((x, 0), T) => Free (x, T)
+      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
+      | Free (x, _) => raise TERM (bad_fixed x, [tm])
+      | t => t)
+  |> Term.map_term_types unvarifyT;
+
+val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
+val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);
+
+val legacy_varify =
+  Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
+  Term.map_term_types legacy_varifyT;
+
+val legacy_unvarify =
+  Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
+  Term.map_term_types legacy_unvarifyT;
 
 
 (* goal states *)

--- a/src/Pure/sign.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/sign.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -721,7 +721,7 @@
 
 fun gen_add_consts prep_typ authentic raw_args thy =
   let
-    val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
+    val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
     fun prep (raw_c, raw_T, raw_mx) =
       let
         val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
@@ -755,7 +755,7 @@
 
     val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
     val c' = Syntax.constN ^ full_name thy c;
-    val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
+    val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val T = Term.fastype_of t;
   in
@@ -772,7 +772,7 @@
   let
     val c = int_const thy raw_c;
     fun prepT raw_T =
-      let val T = Type.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T)))
+      let val T = Logic.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T)))
       in cert_term thy (Const (c, T)); T end
       handle TYPE (msg, _, _) => error msg;
   in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end;

--- a/src/Pure/theory.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/theory.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -240,7 +240,7 @@
     val consts = Sign.consts_of thy;
     fun prep const =
       let val Const (c, T) = Sign.no_vars pp (Const const)
-      in (c, Consts.typargs consts (c, Compress.typ thy (Type.varifyT T))) end;
+      in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end;
 
     val lhs_vars = Term.add_tfreesT (#2 lhs) [];
     val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
@@ -267,7 +267,7 @@
       (case Sign.const_constraint thy c of
         NONE => error ("Undeclared constant " ^ quote c)
       | SOME declT => declT);
-    val T' = Type.varifyT T;
+    val T' = Logic.varifyT T;
 
     fun message txt =
       [Pretty.block [Pretty.str "Specification of constant ",

--- a/src/Pure/type.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/type.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -40,8 +40,6 @@
   (*special treatment of type vars*)
   val strip_sorts: typ -> typ
   val no_tvars: typ -> typ
-  val varifyT: typ -> typ
-  val unvarifyT: typ -> typ
   val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
   val freeze_thaw_type: typ -> typ * (typ -> typ)
   val freeze_type: typ -> typ
@@ -228,10 +226,7 @@
       commas_quote (map (Term.string_of_vname o #1) vs), [T], []));
 
 
-(* varify, unvarify *)
-
-val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
-val unvarifyT = map_type_tvar (fn ((a, 0), S) => TFree (a, S) | v => TVar v);
+(* varify *)
 
 fun varify (t, fixed) =
   let