renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
authorwenzelm
Sat Mar 20 17:33:11 2010 +0100 (2010-03-20)
changeset 35845e5980f0ad025
parent 35844 65258d2c3214
child 35846 2ae4b7585501
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
NEWS
src/HOL/Code_Evaluation.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SMT/Tools/smt_translate.ML
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/rewrite_hol_proof.ML
src/HOL/Tools/typecopy.ML
src/Provers/Arith/abel_cancel.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/code.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/theory_target.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Tools/find_consts.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/conjunction.ML
src/Pure/defs.ML
src/Pure/display.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/logic.ML
src/Pure/meta_simplifier.ML
src/Pure/more_thm.ML
src/Pure/proofterm.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Tools/Code/code_thingol.ML
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/nbe.ML
     1.1 --- a/NEWS	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/NEWS	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -290,6 +290,10 @@
     1.4  Pretty.pp argument to merge, which is absent in the standard
     1.5  Theory_Data version.
     1.6  
     1.7 +* Renamed varify/unvarify operations to varify_global/unvarify_global
     1.8 +to emphasize that these only work in a global situation (which is
     1.9 +quite rare).
    1.10 +
    1.11  
    1.12  *** System ***
    1.13  
     2.1 --- a/src/HOL/Code_Evaluation.thy	Sat Mar 20 02:23:41 2010 +0100
     2.2 +++ b/src/HOL/Code_Evaluation.thy	Sat Mar 20 17:33:11 2010 +0100
     2.3 @@ -87,13 +87,14 @@
     2.4      let
     2.5        val t = list_comb (Const (c, tys ---> ty),
     2.6          map Free (Name.names Name.context "a" tys));
     2.7 -      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
     2.8 -        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
     2.9 +      val (arg, rhs) =
    2.10 +        pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    2.11 +          (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    2.12        val cty = Thm.ctyp_of thy ty;
    2.13      in
    2.14        @{thm term_of_anything}
    2.15        |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    2.16 -      |> Thm.varifyT
    2.17 +      |> Thm.varifyT_global
    2.18      end;
    2.19    fun add_term_of_code tyco raw_vs raw_cs thy =
    2.20      let
    2.21 @@ -131,7 +132,7 @@
    2.22      in
    2.23        @{thm term_of_anything}
    2.24        |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
    2.25 -      |> Thm.varifyT
    2.26 +      |> Thm.varifyT_global
    2.27      end;
    2.28    fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
    2.29      let
     3.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sat Mar 20 02:23:41 2010 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Mar 20 17:33:11 2010 +0100
     3.3 @@ -3438,7 +3438,7 @@
     3.4      | mk_result prec NONE = @{term "UNIV :: real set"}
     3.5  
     3.6    fun realify t = let
     3.7 -      val t = Logic.varify t
     3.8 +      val t = Logic.varify_global t
     3.9        val m = map (fn (name, sort) => (name, @{typ real})) (Term.add_tvars t [])
    3.10        val t = Term.subst_TVars m t
    3.11      in t end
     4.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Mar 20 02:23:41 2010 +0100
     4.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Mar 20 17:33:11 2010 +0100
     4.3 @@ -1418,7 +1418,7 @@
     4.4          val _ = message "INST_TYPE:"
     4.5          val _ = if_debug pth hth
     4.6          val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
     4.7 -        val th1 = Thm.varifyT th
     4.8 +        val th1 = Thm.varifyT_global th
     4.9          val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
    4.10          val tyinst = map (fn (bef, iS) =>
    4.11                               (case try (Lib.assoc (TFree bef)) lambda of
    4.12 @@ -2028,7 +2028,7 @@
    4.13                                   names'
    4.14                                   (thy1,th)
    4.15              val _ = ImportRecorder.add_specification names' th
    4.16 -            val res' = Thm.unvarify res
    4.17 +            val res' = Thm.unvarify_global res
    4.18              val hth = HOLThm(rens,res')
    4.19              val rew = rewrite_hol4_term (concl_of res') thy'
    4.20              val th  = equal_elim rew res'
     5.1 --- a/src/HOL/Import/shuffler.ML	Sat Mar 20 02:23:41 2010 +0100
     5.2 +++ b/src/HOL/Import/shuffler.ML	Sat Mar 20 17:33:11 2010 +0100
     5.3 @@ -265,7 +265,7 @@
     5.4      let
     5.5          val cU = ctyp_of thy U
     5.6          val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
     5.7 -        val (rens, thm') = Thm.varifyT'
     5.8 +        val (rens, thm') = Thm.varifyT_global'
     5.9      (remove (op = o apsnd fst) name tfrees) thm
    5.10          val mid =
    5.11              case rens of
    5.12 @@ -592,7 +592,7 @@
    5.13          fun process [] = NONE
    5.14            | process ((name,th)::thms) =
    5.15              let
    5.16 -                val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
    5.17 +                val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th)))
    5.18                  val triv_th = trivial rhs
    5.19                  val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
    5.20                  val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
     6.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Sat Mar 20 02:23:41 2010 +0100
     6.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Sat Mar 20 17:33:11 2010 +0100
     6.3 @@ -218,7 +218,7 @@
     6.4       val typeSignature = #tsig (Sign.rep_sg consSig)
     6.5     in
     6.6       if ((consNameStr = forbNameStr) 
     6.7 -       andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT forbType))))
     6.8 +       andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT_global forbType))))
     6.9       then true
    6.10       else in_list_forb consSig (consNameStr,consType) xs
    6.11     end;
     7.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 20 02:23:41 2010 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 20 17:33:11 2010 +0100
     7.3 @@ -849,7 +849,7 @@
     7.4  
     7.5      fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
     7.6        let
     7.7 -        val _ $ (_ $ (Rep $ x)) = Logic.unvarify (prop_of th);
     7.8 +        val _ $ (_ $ (Rep $ x)) = Logic.unvarify_global (prop_of th);
     7.9          val Type ("fun", [T, U]) = fastype_of Rep;
    7.10          val permT = mk_permT (Type (atom, []));
    7.11          val pi = Free ("pi", permT);
    7.12 @@ -1394,7 +1394,7 @@
    7.13            (pnames ~~ map head_of (HOLogic.dest_conj
    7.14               (HOLogic.dest_Trueprop (concl_of induct_aux)))) @
    7.15        map (fn (_, f) =>
    7.16 -        let val f' = Logic.varify f
    7.17 +        let val f' = Logic.varify_global f
    7.18          in (cterm_of thy9 f',
    7.19            cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
    7.20          end) fresh_fs) induct_aux;
    7.21 @@ -1677,14 +1677,14 @@
    7.22  
    7.23      val induct_aux_rec = Drule.cterm_instantiate
    7.24        (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
    7.25 -         (map (fn (aT, f) => (Logic.varify f, Abs ("z", HOLogic.unitT,
    7.26 +         (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT,
    7.27              Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
    7.28                fresh_fs @
    7.29            map (fn (((P, T), (x, U)), Q) =>
    7.30 -           (Var ((P, 0), Logic.varifyT (fsT' --> T --> HOLogic.boolT)),
    7.31 +           (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
    7.32              Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
    7.33                (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
    7.34 -          map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T)))
    7.35 +          map (fn (s, T) => (Var ((s, 0), Logic.varifyT_global T), Free (s, T)))
    7.36              rec_unique_frees)) induct_aux;
    7.37  
    7.38      fun obtain_fresh_name vs ths rec_fin_supp T (freshs1, freshs2, ctxt) =
     8.1 --- a/src/HOL/SMT/Tools/smt_translate.ML	Sat Mar 20 02:23:41 2010 +0100
     8.2 +++ b/src/HOL/SMT/Tools/smt_translate.ML	Sat Mar 20 17:33:11 2010 +0100
     8.3 @@ -126,11 +126,11 @@
     8.4    let
     8.5      fun dest (t, bn) =
     8.6        let val (n, T) = Term.dest_Const t
     8.7 -      in (n, (Logic.varifyT T, K (SOME o pair bn))) end
     8.8 +      in (n, (Logic.varifyT_global T, K (SOME o pair bn))) end
     8.9    in Symtab.make (AList.group (op =) (map dest entries)) end
    8.10  
    8.11  fun builtin_add (t, f) tab =
    8.12 -  let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
    8.13 +  let val (n, T) = apsnd Logic.varifyT_global (Term.dest_Const t)
    8.14    in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
    8.15  
    8.16  fun builtin_lookup tab thy (n, T) ts =
     9.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Sat Mar 20 02:23:41 2010 +0100
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sat Mar 20 17:33:11 2010 +0100
     9.3 @@ -46,7 +46,7 @@
     9.4        in
     9.5          SOME {case_name = case_name,
     9.6            constructors = map (fn (cname, dts') =>
     9.7 -            Const (cname, Logic.varifyT (map mk_ty dts' ---> T))) constrs}
     9.8 +            Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs}
     9.9        end
    9.10    | NONE => NONE;
    9.11  
    9.12 @@ -87,7 +87,7 @@
    9.13      val (_, Ty) = dest_Const c
    9.14      val Ts = binder_types Ty;
    9.15      val names = Name.variant_list used
    9.16 -      (Datatype_Prop.make_tnames (map Logic.unvarifyT Ts));
    9.17 +      (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
    9.18      val ty = body_type Ty;
    9.19      val ty_theta = ty_match ty colty handle Type.TYPE_MATCH =>
    9.20        raise CASE_ERROR ("type mismatch", ~1)
    10.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Sat Mar 20 02:23:41 2010 +0100
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Sat Mar 20 17:33:11 2010 +0100
    10.3 @@ -310,7 +310,7 @@
    10.4        (#case_rewrites o Datatype_Data.the_info thy) tyco;
    10.5      val thms as hd_thm :: _ = raw_thms
    10.6        |> Conjunction.intr_balanced
    10.7 -      |> Thm.unvarify
    10.8 +      |> Thm.unvarify_global
    10.9        |> Conjunction.elim_balanced (length raw_thms)
   10.10        |> map Simpdata.mk_meta_eq
   10.11        |> map Drule.zero_var_indexes
   10.12 @@ -332,7 +332,7 @@
   10.13      |> Thm.implies_intr asm
   10.14      |> Thm.generalize ([], params) 0
   10.15      |> AxClass.unoverload thy
   10.16 -    |> Thm.varifyT
   10.17 +    |> Thm.varifyT_global
   10.18    end;
   10.19  
   10.20  
    11.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 20 02:23:41 2010 +0100
    11.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 20 17:33:11 2010 +0100
    11.3 @@ -128,7 +128,7 @@
    11.4          (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
    11.5        ||> Sign.restore_naming thy;
    11.6  
    11.7 -    val ivs = rev (Term.add_vars (Logic.varify (Datatype_Prop.make_ind [descr] sorts)) []);
    11.8 +    val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
    11.9      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
   11.10      val ivs1 = map Var (filter_out (fn (_, T) =>  (* FIXME set (!??) *)
   11.11        tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs);
   11.12 @@ -139,7 +139,7 @@
   11.13          (fold_rev (fn (f, p) => fn prf =>
   11.14            (case head_of (strip_abs_body f) of
   11.15               Free (s, T) =>
   11.16 -               let val T' = Logic.varifyT T
   11.17 +               let val T' = Logic.varifyT_global T
   11.18                 in Abst (s, SOME T', Proofterm.prf_abstract_over
   11.19                   (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
   11.20                 end
   11.21 @@ -149,8 +149,8 @@
   11.22  
   11.23      val r' =
   11.24        if null is then r
   11.25 -      else Logic.varify (fold_rev lambda
   11.26 -        (map Logic.unvarify ivs1 @ filter_out is_unit
   11.27 +      else Logic.varify_global (fold_rev lambda
   11.28 +        (map Logic.unvarify_global ivs1 @ filter_out is_unit
   11.29              (map (head_of o strip_abs_body) rec_fns)) r);
   11.30  
   11.31    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
   11.32 @@ -179,7 +179,7 @@
   11.33      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
   11.34      val r = Const (case_name, map fastype_of rs ---> T --> rT);
   11.35  
   11.36 -    val y = Var (("y", 0), Logic.varifyT T);
   11.37 +    val y = Var (("y", 0), Logic.varifyT_global T);
   11.38      val y' = Free ("y", T);
   11.39  
   11.40      val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
   11.41 @@ -200,10 +200,10 @@
   11.42      val P = Var (("P", 0), rT' --> HOLogic.boolT);
   11.43      val prf = forall_intr_prf (y, forall_intr_prf (P,
   11.44        fold_rev (fn (p, r) => fn prf =>
   11.45 -          forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), prf)))
   11.46 +          forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf)))
   11.47          (prems ~~ rs)
   11.48          (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
   11.49 -    val r' = Logic.varify (Abs ("y", T,
   11.50 +    val r' = Logic.varify_global (Abs ("y", T,
   11.51        list_abs (map dest_Free rs, list_comb (r,
   11.52          map Bound ((length rs - 1 downto 0) @ [length rs])))));
   11.53  
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 20 02:23:41 2010 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 20 17:33:11 2010 +0100
    12.3 @@ -566,7 +566,7 @@
    12.4      SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
    12.5            Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
    12.6            set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
    12.7 -                          |> Logic.varify,
    12.8 +                          |> Logic.varify_global,
    12.9            set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   12.10    else case Typedef.get_info_global thy s of
   12.11      (* FIXME handle multiple typedef interpretations (!??) *)
   12.12 @@ -599,7 +599,7 @@
   12.13    handle Type.TYPE_MATCH =>
   12.14           raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
   12.15  fun varify_and_instantiate_type thy T1 T1' T2 =
   12.16 -  instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2)
   12.17 +  instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2)
   12.18  
   12.19  (* theory -> typ -> typ -> styp *)
   12.20  fun repair_constr_type thy body_T' T =
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Mar 20 02:23:41 2010 +0100
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Mar 20 17:33:11 2010 +0100
    13.3 @@ -326,7 +326,7 @@
    13.4  
    13.5  (* theory -> typ * typ -> bool *)
    13.6  fun varified_type_match thy (candid_T, pat_T) =
    13.7 -  strict_type_match thy (candid_T, Logic.varifyT pat_T)
    13.8 +  strict_type_match thy (candid_T, Logic.varifyT_global pat_T)
    13.9  
   13.10  (* atom_pool -> (string * string) * (string * string) -> scope -> nut list
   13.11     -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
    14.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Mar 20 02:23:41 2010 +0100
    14.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Mar 20 17:33:11 2010 +0100
    14.3 @@ -404,7 +404,7 @@
    14.4    (let
    14.5       val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
    14.6       fun varify (t, (i, ts)) =
    14.7 -       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t))
    14.8 +       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
    14.9         in (maxidx_of_term t', t'::ts) end;
   14.10       val (i, cs') = List.foldr varify (~1, []) cs;
   14.11       val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
    15.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sat Mar 20 02:23:41 2010 +0100
    15.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sat Mar 20 17:33:11 2010 +0100
    15.3 @@ -87,7 +87,7 @@
    15.4  (* theory -> term -> (string list, term list list) *)
    15.5  
    15.6  fun dest_code_eqn eqn = let
    15.7 -  val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn))
    15.8 +  val (lhs, rhs) = Logic.dest_equals (Logic.unvarify_global (Thm.prop_of eqn))
    15.9    val (func, args) = strip_comb lhs
   15.10  in ((func, args), rhs) end;
   15.11  
   15.12 @@ -372,7 +372,7 @@
   15.13              *)
   15.14              
   15.15              val thy'' = Fun_Pred.map
   15.16 -              (fold Item_Net.update (map (apfst Logic.varify)
   15.17 +              (fold Item_Net.update (map (apfst Logic.varify_global)
   15.18                  (distinct (op =) funs ~~ (#preds ind_result)))) thy'
   15.19              (*val _ = print_specs thy'' specs*)
   15.20            in
   15.21 @@ -397,7 +397,7 @@
   15.22      | lookup_pred _ = NONE
   15.23      *)
   15.24      fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
   15.25 -    val intro_t = (Logic.unvarify o prop_of) intro
   15.26 +    val intro_t = Logic.unvarify_global (prop_of intro)
   15.27      val (prems, concl) = Logic.strip_horn intro_t
   15.28      val frees = map fst (Term.add_frees intro_t [])
   15.29      fun rewrite prem names =
    16.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Mar 20 02:23:41 2010 +0100
    16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Mar 20 17:33:11 2010 +0100
    16.3 @@ -313,7 +313,7 @@
    16.4          fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
    16.5            let
    16.6              val vars = map Var (Term.add_vars abs_arg [])
    16.7 -            val abs_arg' = Logic.unvarify abs_arg
    16.8 +            val abs_arg' = Logic.unvarify_global abs_arg
    16.9              val frees = map Free (Term.add_frees abs_arg' [])
   16.10              val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
   16.11                ((Long_Name.base_name constname) ^ "_hoaux")
   16.12 @@ -326,7 +326,8 @@
   16.13                |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
   16.14                |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
   16.15            in
   16.16 -            (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy'))
   16.17 +            (list_comb (Logic.varify_global const, vars),
   16.18 +              ((full_constname, [definition])::new_defs, thy'))
   16.19            end
   16.20          | replace_abs_arg arg (new_defs, thy) =
   16.21            if (is_predT (fastype_of arg)) then
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Mar 20 02:23:41 2010 +0100
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Mar 20 17:33:11 2010 +0100
    17.3 @@ -267,7 +267,7 @@
    17.4    in  Goal.prove_internal [ex_tm] conc tacf
    17.5         |> forall_intr_list frees
    17.6         |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
    17.7 -       |> Thm.varifyT
    17.8 +       |> Thm.varifyT_global
    17.9    end;
   17.10  
   17.11  
    18.1 --- a/src/HOL/Tools/choice_specification.ML	Sat Mar 20 02:23:41 2010 +0100
    18.2 +++ b/src/HOL/Tools/choice_specification.ML	Sat Mar 20 17:33:11 2010 +0100
    18.3 @@ -90,9 +90,9 @@
    18.4    | collect_consts (tm as Const _,tms) = insert (op aconv) tm tms
    18.5    | collect_consts (            _,tms) = tms
    18.6  
    18.7 -(* Complementing Type.varify... *)
    18.8 +(* Complementing Type.varify_global... *)
    18.9  
   18.10 -fun unvarify t fmap =
   18.11 +fun unvarify_global t fmap =
   18.12      let
   18.13          val fmap' = map Library.swap fmap
   18.14          fun unthaw (f as (a, S)) =
   18.15 @@ -135,7 +135,7 @@
   18.16          val prop  = myfoldr HOLogic.mk_conj (map fst props'')
   18.17          val cprop = cterm_of thy (HOLogic.mk_Trueprop prop)
   18.18  
   18.19 -        val (vmap, prop_thawed) = Type.varify [] prop
   18.20 +        val (vmap, prop_thawed) = Type.varify_global [] prop
   18.21          val thawed_prop_consts = collect_consts (prop_thawed,[])
   18.22          val (altcos,overloaded) = Library.split_list cos
   18.23          val (names,sconsts) = Library.split_list altcos
   18.24 @@ -145,14 +145,14 @@
   18.25  
   18.26          fun proc_const c =
   18.27              let
   18.28 -                val (_, c') = Type.varify [] c
   18.29 +                val (_, c') = Type.varify_global [] c
   18.30                  val (cname,ctyp) = dest_Const c'
   18.31              in
   18.32                  case filter (fn t => let val (name,typ) = dest_Const t
   18.33                                       in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
   18.34                                       end) thawed_prop_consts of
   18.35                      [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found")
   18.36 -                  | [cf] => unvarify cf vmap
   18.37 +                  | [cf] => unvarify_global cf vmap
   18.38                    | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)")
   18.39              end
   18.40          val proc_consts = map proc_const consts
    19.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 20 02:23:41 2010 +0100
    19.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 20 17:33:11 2010 +0100
    19.3 @@ -70,9 +70,9 @@
    19.4      val params = map dest_Var (take nparms ts);
    19.5      val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
    19.6      fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
    19.7 -      map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
    19.8 +      map (Logic.unvarifyT_global o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
    19.9          filter_out (equal Extraction.nullT) (map
   19.10 -          (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
   19.11 +          (Logic.unvarifyT_global o Extraction.etype_of thy vs []) (prems_of intr)),
   19.12              NoSyn);
   19.13    in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
   19.14      map constr_of_intr intrs)
   19.15 @@ -339,13 +339,13 @@
   19.16          let
   19.17            val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
   19.18            val s' = Long_Name.base_name s;
   19.19 -          val T' = Logic.unvarifyT T;
   19.20 +          val T' = Logic.unvarifyT_global T;
   19.21          in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
   19.22        |> distinct (op = o pairself (#1 o #1))
   19.23        |> map (apfst (apfst (apfst Binding.name)))
   19.24        |> split_list;
   19.25  
   19.26 -    val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
   19.27 +    val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT_global T))
   19.28        (List.take (snd (strip_comb
   19.29          (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
   19.30  
   19.31 @@ -357,7 +357,7 @@
   19.32            no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
   19.33          rlzpreds rlzparams (map (fn (rintr, intr) =>
   19.34            ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
   19.35 -           subst_atomic rlzpreds' (Logic.unvarify rintr)))
   19.36 +           subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
   19.37               (rintrs ~~ maps snd rss)) [] ||>
   19.38        Sign.root_path;
   19.39      val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
   19.40 @@ -383,7 +383,7 @@
   19.41            (used @ rnames) (replicate (length intrs) "s");
   19.42          val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
   19.43            let
   19.44 -            val (P, Q) = strip_one name (Logic.unvarify rlz);
   19.45 +            val (P, Q) = strip_one name (Logic.unvarify_global rlz);
   19.46              val Q' = strip_all' [] rnames' Q
   19.47            in
   19.48              (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
   19.49 @@ -446,7 +446,7 @@
   19.50              map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   19.51              [Bound (length prems)]));
   19.52          val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
   19.53 -        val rlz' = strip_all (Logic.unvarify rlz);
   19.54 +        val rlz' = strip_all (Logic.unvarify_global rlz);
   19.55          val rews = map mk_meta_eq case_thms;
   19.56          val thm = Goal.prove_global thy []
   19.57            (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
    20.1 --- a/src/HOL/Tools/meson.ML	Sat Mar 20 02:23:41 2010 +0100
    20.2 +++ b/src/HOL/Tools/meson.ML	Sat Mar 20 17:33:11 2010 +0100
    20.3 @@ -667,7 +667,7 @@
    20.4  fun make_meta_clause th =
    20.5    let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
    20.6    in  
    20.7 -      (zero_var_indexes o Thm.varifyT o thaw 0 o 
    20.8 +      (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
    20.9         negated_asm_of_head o make_horn resolution_clause_rules) fth
   20.10    end;
   20.11  
    21.1 --- a/src/HOL/Tools/old_primrec.ML	Sat Mar 20 02:23:41 2010 +0100
    21.2 +++ b/src/HOL/Tools/old_primrec.ML	Sat Mar 20 17:33:11 2010 +0100
    21.3 @@ -35,7 +35,7 @@
    21.4  fun unify_consts thy cs intr_ts =
    21.5    (let
    21.6      fun varify t (i, ts) =
    21.7 -      let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
    21.8 +      let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify_global [] t))
    21.9        in (maxidx_of_term t', t'::ts) end;
   21.10      val (i, cs') = fold_rev varify cs (~1, []);
   21.11      val (i', intr_ts') = fold_rev varify intr_ts (i, []);
   21.12 @@ -281,7 +281,7 @@
   21.13        thy'
   21.14        |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
   21.15      val simps'' = maps snd simps';
   21.16 -    val lhss = map (Logic.varify o fst o Logic.dest_equals o snd) defs';
   21.17 +    val lhss = map (Logic.varify_global o fst o Logic.dest_equals o snd) defs';
   21.18    in
   21.19      thy''
   21.20      |> note (("simps",
    22.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Sat Mar 20 02:23:41 2010 +0100
    22.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Mar 20 17:33:11 2010 +0100
    22.3 @@ -316,7 +316,7 @@
    22.4  fun perhaps_constrain thy insts raw_vs =
    22.5    let
    22.6      fun meet_random (T, sort) = Sorts.meet_sort (Sign.classes_of thy) 
    22.7 -      (Logic.varifyT T, sort);
    22.8 +      (Logic.varifyT_global T, sort);
    22.9      val vtab = Vartab.empty
   22.10        |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
   22.11        |> fold meet_random insts;
    23.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Sat Mar 20 02:23:41 2010 +0100
    23.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sat Mar 20 17:33:11 2010 +0100
    23.3 @@ -16,7 +16,7 @@
    23.4  open Proofterm;
    23.5  
    23.6  val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
    23.7 -    Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT)
    23.8 +    Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT)
    23.9  
   23.10    (** eliminate meta-equality rules **)
   23.11  
    24.1 --- a/src/HOL/Tools/typecopy.ML	Sat Mar 20 02:23:41 2010 +0100
    24.2 +++ b/src/HOL/Tools/typecopy.ML	Sat Mar 20 17:33:11 2010 +0100
    24.3 @@ -61,7 +61,7 @@
    24.4          let
    24.5            val exists_thm =
    24.6              UNIV_I
    24.7 -            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
    24.8 +            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] [];
    24.9            val inject' = inject OF [exists_thm, exists_thm];
   24.10            val proj_def = inverse OF [exists_thm];
   24.11            val info = {
   24.12 @@ -95,7 +95,7 @@
   24.13        typ = ty_rep, ... } = get_info thy tyco;
   24.14      (* FIXME handle multiple typedef interpretations (!??) *)
   24.15      val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco;
   24.16 -    val constr = (c, Logic.unvarifyT (Sign.the_const_type thy c));
   24.17 +    val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
   24.18      val ty = Type (tyco, map TFree vs);
   24.19      val proj = Const (proj, ty --> ty_rep);
   24.20      val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
   24.21 @@ -109,7 +109,7 @@
   24.22            THEN ALLGOALS (rtac @{thm refl});
   24.23      fun mk_eq_refl thy = @{thm HOL.eq_refl}
   24.24        |> Thm.instantiate
   24.25 -         ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
   24.26 +         ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], [])
   24.27        |> AxClass.unoverload thy;
   24.28    in
   24.29      thy
    25.1 --- a/src/Provers/Arith/abel_cancel.ML	Sat Mar 20 02:23:41 2010 +0100
    25.2 +++ b/src/Provers/Arith/abel_cancel.ML	Sat Mar 20 17:33:11 2010 +0100
    25.3 @@ -88,7 +88,7 @@
    25.4  
    25.5  val sum_conv =
    25.6    Simplifier.mk_simproc "cancel_sums"
    25.7 -    (map (Drule.cterm_fun Logic.varify) Data.sum_pats) (K sum_proc);
    25.8 +    (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc);
    25.9  
   25.10  
   25.11  (*A simproc to cancel like terms on the opposite sides of relations:
    26.1 --- a/src/Pure/Isar/class.ML	Sat Mar 20 02:23:41 2010 +0100
    26.2 +++ b/src/Pure/Isar/class.ML	Sat Mar 20 17:33:11 2010 +0100
    26.3 @@ -257,7 +257,7 @@
    26.4          | t => t);
    26.5      val raw_pred = Locale.intros_of thy class
    26.6        |> fst
    26.7 -      |> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
    26.8 +      |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
    26.9      fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
   26.10       of [] => NONE
   26.11        | [thm] => SOME thm;
    27.1 --- a/src/Pure/Isar/class_target.ML	Sat Mar 20 02:23:41 2010 +0100
    27.2 +++ b/src/Pure/Isar/class_target.ML	Sat Mar 20 17:33:11 2010 +0100
    27.3 @@ -332,7 +332,7 @@
    27.4      |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
    27.5      |> snd
    27.6      |> Thm.add_def false false (b_def, def_eq)
    27.7 -    |>> Thm.varifyT
    27.8 +    |>> Thm.varifyT_global
    27.9      |-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
   27.10        #> snd
   27.11        #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
   27.12 @@ -347,7 +347,7 @@
   27.13      val c' = Sign.full_name thy b;
   27.14      val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
   27.15      val ty' = Term.fastype_of rhs';
   27.16 -    val rhs'' = map_types Logic.varifyT rhs';
   27.17 +    val rhs'' = map_types Logic.varifyT_global rhs';
   27.18    in
   27.19      thy
   27.20      |> Sign.add_abbrev (#1 prmode) (b, rhs'')
   27.21 @@ -530,7 +530,7 @@
   27.22      val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   27.23      val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
   27.24      fun after_qed' results =
   27.25 -      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   27.26 +      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
   27.27        #> after_qed;
   27.28    in
   27.29      lthy
    28.1 --- a/src/Pure/Isar/code.ML	Sat Mar 20 02:23:41 2010 +0100
    28.2 +++ b/src/Pure/Isar/code.ML	Sat Mar 20 17:33:11 2010 +0100
    28.3 @@ -337,7 +337,7 @@
    28.4          (Binding.qualified_name tyco, n) | _ => I) decls
    28.5    end;
    28.6  
    28.7 -fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars;
    28.8 +fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
    28.9  
   28.10  fun read_signature thy = cert_signature thy o Type.strip_sorts
   28.11    o Syntax.parse_typ (ProofContext.init thy);
   28.12 @@ -374,7 +374,7 @@
   28.13    let
   28.14      val _ = Thm.cterm_of thy (Const (c, raw_ty));
   28.15      val ty = subst_signature thy c raw_ty;
   28.16 -    val ty_decl = (Logic.unvarifyT o const_typ thy) c;
   28.17 +    val ty_decl = (Logic.unvarifyT_global o const_typ thy) c;
   28.18      fun last_typ c_ty ty =
   28.19        let
   28.20          val tfrees = Term.add_tfreesT ty [];
   28.21 @@ -684,7 +684,7 @@
   28.22        (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
   28.23    in
   28.24      thm
   28.25 -    |> Thm.varifyT
   28.26 +    |> Thm.varifyT_global
   28.27      |> Thm.certify_instantiate (inst, [])
   28.28      |> pair subst
   28.29    end;
   28.30 @@ -697,7 +697,7 @@
   28.31      val ty_abs = (fastype_of o snd o dest_comb) lhs;
   28.32      val abs = Thm.cterm_of thy (Const (c, ty --> ty_abs));
   28.33      val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm];
   28.34 -  in (c, (Thm.varifyT o zero_var_indexes) raw_concrete_thm) end;
   28.35 +  in (c, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end;
   28.36  
   28.37  fun add_rhss_of_eqn thy t =
   28.38    let
   28.39 @@ -706,7 +706,8 @@
   28.40        | add_const _ = I
   28.41    in fold_aterms add_const t end;
   28.42  
   28.43 -fun dest_eqn thy = apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy o Logic.unvarify;
   28.44 +fun dest_eqn thy =
   28.45 +  apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy o Logic.unvarify_global;
   28.46  
   28.47  abstype cert = Equations of thm * bool list
   28.48    | Projection of term * string
   28.49 @@ -811,14 +812,14 @@
   28.50          val thms = if null propers then [] else
   28.51            cert_thm
   28.52            |> Local_Defs.expand [snd (get_head thy cert_thm)]
   28.53 -          |> Thm.varifyT
   28.54 +          |> Thm.varifyT_global
   28.55            |> Conjunction.elim_balanced (length propers);
   28.56        in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
   28.57    | equations_of_cert thy (Projection (t, tyco)) =
   28.58        let
   28.59          val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
   28.60          val tyscm = typscheme_projection thy t;
   28.61 -        val t' = map_types Logic.varifyT t;
   28.62 +        val t' = map_types Logic.varifyT_global t;
   28.63        in (tyscm, [((SOME abs, dest_eqn thy t'), (NONE, true))]) end
   28.64    | equations_of_cert thy (Abstract (abs_thm, tyco)) =
   28.65        let
   28.66 @@ -827,22 +828,24 @@
   28.67          val _ = fold_aterms (fn Const (c, _) => if c = abs
   28.68            then error ("Abstraction violation in abstract code equation\n" ^ Display.string_of_thm_global thy abs_thm)
   28.69            else I | _ => I) (Thm.prop_of abs_thm);
   28.70 -      in (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT abs_thm), true))]) end;
   28.71 +      in
   28.72 +        (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT_global abs_thm), true))])
   28.73 +      end;
   28.74  
   28.75  fun pretty_cert thy (cert as Equations _) =
   28.76        (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)
   28.77           o snd o equations_of_cert thy) cert
   28.78    | pretty_cert thy (Projection (t, _)) =
   28.79 -      [Syntax.pretty_term_global thy (map_types Logic.varifyT t)]
   28.80 +      [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)]
   28.81    | pretty_cert thy (Abstract (abs_thm, tyco)) =
   28.82 -      [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT) abs_thm];
   28.83 +      [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
   28.84  
   28.85  fun bare_thms_of_cert thy (cert as Equations _) =
   28.86        (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
   28.87          o snd o equations_of_cert thy) cert
   28.88    | bare_thms_of_cert thy (Projection _) = []
   28.89    | bare_thms_of_cert thy (Abstract (abs_thm, tyco)) =
   28.90 -      [Thm.varifyT (snd (concretify_abs thy tyco abs_thm))];
   28.91 +      [Thm.varifyT_global (snd (concretify_abs thy tyco abs_thm))];
   28.92  
   28.93  end;
   28.94  
   28.95 @@ -1157,7 +1160,7 @@
   28.96        (del_eqns abs
   28.97        #> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
   28.98        #> change_fun_spec false rep ((K o Proj)
   28.99 -        (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco))
  28.100 +        (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco))
  28.101        #> Abstype_Interpretation.data (tyco, serial ()));
  28.102    in
  28.103      thy
    29.1 --- a/src/Pure/Isar/constdefs.ML	Sat Mar 20 02:23:41 2010 +0100
    29.2 +++ b/src/Pure/Isar/constdefs.ML	Sat Mar 20 17:33:11 2010 +0100
    29.3 @@ -56,7 +56,7 @@
    29.4        |> Sign.add_consts_i [(b, T, mx)]
    29.5        |> PureThy.add_defs false [((name, def), atts)]
    29.6        |-> (fn [thm] =>  (* FIXME thm vs. atts !? *)
    29.7 -        Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #>
    29.8 +        Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify_global head], [thm]) #>
    29.9          Code.add_default_eqn thm);
   29.10    in ((c, T), thy') end;
   29.11  
    30.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 20 02:23:41 2010 +0100
    30.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 20 17:33:11 2010 +0100
    30.3 @@ -162,7 +162,7 @@
    30.4      val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
    30.5  
    30.6      (* type inference and contexts *)
    30.7 -    val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
    30.8 +    val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT_global) parm_types;
    30.9      val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   30.10      val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   30.11      val res = Syntax.check_terms ctxt arg;
   30.12 @@ -346,7 +346,7 @@
   30.13          val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   30.14          val inst' = prep_inst ctxt parm_names inst;
   30.15          val parm_types' = map (TypeInfer.paramify_vars o
   30.16 -          Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
   30.17 +          Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
   30.18          val inst'' = map2 TypeInfer.constrain parm_types' inst';
   30.19          val insts' = insts @ [(loc, (prfx, inst''))];
   30.20          val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
    31.1 --- a/src/Pure/Isar/obtain.ML	Sat Mar 20 02:23:41 2010 +0100
    31.2 +++ b/src/Pure/Isar/obtain.ML	Sat Mar 20 17:33:11 2010 +0100
    31.3 @@ -197,7 +197,7 @@
    31.4  
    31.5      val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
    31.6      val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
    31.7 -    val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
    31.8 +    val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
    31.9      val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
   31.10      val (prems, ctxt'') =
   31.11        Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
   31.12 @@ -252,7 +252,7 @@
   31.13      val vars' =
   31.14        map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
   31.15        (map snd vars @ replicate (length ys) NoSyn);
   31.16 -    val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
   31.17 +    val rule'' = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
   31.18    in ((vars', rule''), ctxt') end;
   31.19  
   31.20  fun inferred_type (binding, _, mx) ctxt =
    32.1 --- a/src/Pure/Isar/theory_target.ML	Sat Mar 20 02:23:41 2010 +0100
    32.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Mar 20 17:33:11 2010 +0100
    32.3 @@ -227,7 +227,7 @@
    32.4       (if is_locale then
    32.5          Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
    32.6          #-> (fn (lhs, _) =>
    32.7 -          let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    32.8 +          let val lhs' = Term.list_comb (Logic.unvarify_global lhs, xs) in
    32.9              syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #>
   32.10              is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
   32.11            end)
    33.1 --- a/src/Pure/Proof/extraction.ML	Sat Mar 20 02:23:41 2010 +0100
    33.2 +++ b/src/Pure/Proof/extraction.ML	Sat Mar 20 17:33:11 2010 +0100
    33.3 @@ -206,7 +206,7 @@
    33.4  fun read_condeq thy =
    33.5    let val thy' = add_syntax thy
    33.6    in fn s =>
    33.7 -    let val t = Logic.varify (Syntax.read_prop_global thy' s)
    33.8 +    let val t = Logic.varify_global (Syntax.read_prop_global thy' s)
    33.9      in
   33.10        (map Logic.dest_equals (Logic.strip_imp_prems t),
   33.11          Logic.dest_equals (Logic.strip_imp_concl t))
   33.12 @@ -732,7 +732,7 @@
   33.13             in
   33.14               thy'
   33.15               |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
   33.16 -                  Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
   33.17 +                  Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
   33.18                      (Thm.forall_elim_var 0) (forall_intr_frees
   33.19                        (ProofChecker.thm_of_proof thy'
   33.20                         (fst (Proofterm.freeze_thaw_prf prf))))))
    34.1 --- a/src/Pure/Proof/proof_syntax.ML	Sat Mar 20 02:23:41 2010 +0100
    34.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sat Mar 20 17:33:11 2010 +0100
    34.3 @@ -217,7 +217,7 @@
    34.4  
    34.5  fun read_proof thy =
    34.6    let val rd = read_term thy proofT
    34.7 -  in fn ty => fn s => proof_of_term thy ty (Logic.varify (rd s)) end;
    34.8 +  in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end;
    34.9  
   34.10  fun proof_syntax prf =
   34.11    let
    35.1 --- a/src/Pure/Proof/proofchecker.ML	Sat Mar 20 02:23:41 2010 +0100
    35.2 +++ b/src/Pure/Proof/proofchecker.ML	Sat Mar 20 17:33:11 2010 +0100
    35.3 @@ -36,7 +36,7 @@
    35.4      fun thm_of_atom thm Ts =
    35.5        let
    35.6          val tvars = OldTerm.term_tvars (Thm.full_prop_of thm);
    35.7 -        val (fmap, thm') = Thm.varifyT' [] thm;
    35.8 +        val (fmap, thm') = Thm.varifyT_global' [] thm;
    35.9          val ctye = map (pairself (Thm.ctyp_of thy))
   35.10            (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
   35.11        in
    36.1 --- a/src/Pure/Tools/find_consts.ML	Sat Mar 20 02:23:41 2010 +0100
    36.2 +++ b/src/Pure/Tools/find_consts.ML	Sat Mar 20 17:33:11 2010 +0100
    36.3 @@ -68,7 +68,7 @@
    36.4  
    36.5  fun pretty_const ctxt (nm, ty) =
    36.6    let
    36.7 -    val ty' = Logic.unvarifyT ty;
    36.8 +    val ty' = Logic.unvarifyT_global ty;
    36.9    in
   36.10      Pretty.block
   36.11       [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    37.1 --- a/src/Pure/axclass.ML	Sat Mar 20 02:23:41 2010 +0100
    37.2 +++ b/src/Pure/axclass.ML	Sat Mar 20 17:33:11 2010 +0100
    37.3 @@ -309,7 +309,7 @@
    37.4      |-> (fn const' as Const (c'', _) =>
    37.5        Thm.add_def false true
    37.6          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
    37.7 -      #>> Thm.varifyT
    37.8 +      #>> Thm.varifyT_global
    37.9        #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
   37.10        #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
   37.11        #> snd
    38.1 --- a/src/Pure/codegen.ML	Sat Mar 20 02:23:41 2010 +0100
    38.2 +++ b/src/Pure/codegen.ML	Sat Mar 20 17:33:11 2010 +0100
    38.3 @@ -474,7 +474,7 @@
    38.4  (**** retrieve definition of constant ****)
    38.5  
    38.6  fun is_instance T1 T2 =
    38.7 -  Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT T2);
    38.8 +  Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT_global T2);
    38.9  
   38.10  fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
   38.11    s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
    39.1 --- a/src/Pure/conjunction.ML	Sat Mar 20 02:23:41 2010 +0100
    39.2 +++ b/src/Pure/conjunction.ML	Sat Mar 20 17:33:11 2010 +0100
    39.3 @@ -75,7 +75,8 @@
    39.4  val A_B = read_prop "A &&& B";
    39.5  
    39.6  val conjunction_def =
    39.7 -  Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
    39.8 +  Thm.unvarify_global
    39.9 +    (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
   39.10  
   39.11  fun conjunctionD which =
   39.12    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
    40.1 --- a/src/Pure/defs.ML	Sat Mar 20 02:23:41 2010 +0100
    40.2 +++ b/src/Pure/defs.ML	Sat Mar 20 17:33:11 2010 +0100
    40.3 @@ -34,7 +34,7 @@
    40.4    let
    40.5      val prt_args =
    40.6        if null args then []
    40.7 -      else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT) args)];
    40.8 +      else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT_global) args)];
    40.9    in Pretty.block (Pretty.str c :: prt_args) end;
   40.10  
   40.11  fun plain_args args =
    41.1 --- a/src/Pure/display.ML	Sat Mar 20 02:23:41 2010 +0100
    41.2 +++ b/src/Pure/display.ML	Sat Mar 20 17:33:11 2010 +0100
    41.3 @@ -131,9 +131,9 @@
    41.4      fun prt_sort S = Syntax.pretty_sort ctxt S;
    41.5      fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
    41.6      fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
    41.7 -    val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
    41.8 +    val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
    41.9      fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
   41.10 -    val prt_term_no_vars = prt_term o Logic.unvarify;
   41.11 +    val prt_term_no_vars = prt_term o Logic.unvarify_global;
   41.12      fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
   41.13      val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
   41.14  
    42.1 --- a/src/Pure/drule.ML	Sat Mar 20 02:23:41 2010 +0100
    42.2 +++ b/src/Pure/drule.ML	Sat Mar 20 17:33:11 2010 +0100
    42.3 @@ -312,7 +312,7 @@
    42.4      Thm.forall_elim_vars (maxidx + 1)
    42.5      #> Thm.strip_shyps
    42.6      #> zero_var_indexes
    42.7 -    #> Thm.varifyT);
    42.8 +    #> Thm.varifyT_global);
    42.9  
   42.10  val export_without_context =
   42.11    flexflex_unique
   42.12 @@ -691,7 +691,7 @@
   42.13  
   42.14  local
   42.15    val A = certify (Free ("A", propT));
   42.16 -  val axiom = Thm.unvarify o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
   42.17 +  val axiom = Thm.unvarify_global o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
   42.18    val prop_def = axiom "Pure.prop_def";
   42.19    val term_def = axiom "Pure.term_def";
   42.20    val sort_constraint_def = axiom "Pure.sort_constraint_def";
   42.21 @@ -762,7 +762,8 @@
   42.22  val sort_constraint_eq =
   42.23    store_standard_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
   42.24      (Thm.equal_intr
   42.25 -      (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
   42.26 +      (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
   42.27 +        (Thm.unvarify_global sort_constraintI)))
   42.28        (implies_intr_list [A, C] (Thm.assume A)));
   42.29  
   42.30  end;
    43.1 --- a/src/Pure/goal.ML	Sat Mar 20 02:23:41 2010 +0100
    43.2 +++ b/src/Pure/goal.ML	Sat Mar 20 17:33:11 2010 +0100
    43.3 @@ -129,7 +129,8 @@
    43.4      val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
    43.5  
    43.6      val global_prop =
    43.7 -      cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
    43.8 +      cert (Term.map_types Logic.varifyT_global
    43.9 +        (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
   43.10        |> Thm.weaken_sorts (Variable.sorts_of ctxt);
   43.11      val global_result = result |> Future.map
   43.12        (Drule.flexflex_unique #>
    44.1 --- a/src/Pure/logic.ML	Sat Mar 20 02:23:41 2010 +0100
    44.2 +++ b/src/Pure/logic.ML	Sat Mar 20 17:33:11 2010 +0100
    44.3 @@ -68,10 +68,10 @@
    44.4    val list_rename_params: string list * term -> term
    44.5    val assum_pairs: int * term -> (term*term)list
    44.6    val assum_problems: int * term -> (term -> term) * term list * term
    44.7 -  val varifyT: typ -> typ
    44.8 -  val unvarifyT: typ -> typ
    44.9 -  val varify: term -> term
   44.10 -  val unvarify: term -> term
   44.11 +  val varifyT_global: typ -> typ
   44.12 +  val unvarifyT_global: typ -> typ
   44.13 +  val varify_global: term -> term
   44.14 +  val unvarify_global: term -> term
   44.15    val get_goal: term -> int -> term
   44.16    val goal_params: term -> int -> term * term list
   44.17    val prems_of_goal: term -> int -> term list
   44.18 @@ -465,35 +465,35 @@
   44.19  fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
   44.20  fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
   44.21  
   44.22 -fun varifyT_same ty = ty
   44.23 +fun varifyT_global_same ty = ty
   44.24    |> Term_Subst.map_atypsT_same
   44.25      (fn TFree (a, S) => TVar ((a, 0), S)
   44.26        | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
   44.27  
   44.28 -fun unvarifyT_same ty = ty
   44.29 +fun unvarifyT_global_same ty = ty
   44.30    |> Term_Subst.map_atypsT_same
   44.31      (fn TVar ((a, 0), S) => TFree (a, S)
   44.32        | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
   44.33        | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
   44.34  
   44.35 -val varifyT = Same.commit varifyT_same;
   44.36 -val unvarifyT = Same.commit unvarifyT_same;
   44.37 +val varifyT_global = Same.commit varifyT_global_same;
   44.38 +val unvarifyT_global = Same.commit unvarifyT_global_same;
   44.39  
   44.40 -fun varify tm = tm
   44.41 +fun varify_global tm = tm
   44.42    |> Same.commit (Term_Subst.map_aterms_same
   44.43      (fn Free (x, T) => Var ((x, 0), T)
   44.44        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   44.45        | _ => raise Same.SAME))
   44.46 -  |> Same.commit (Term_Subst.map_types_same varifyT_same)
   44.47 +  |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
   44.48    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   44.49  
   44.50 -fun unvarify tm = tm
   44.51 +fun unvarify_global tm = tm
   44.52    |> Same.commit (Term_Subst.map_aterms_same
   44.53      (fn Var ((x, 0), T) => Free (x, T)
   44.54        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   44.55        | Free (x, _) => raise TERM (bad_fixed x, [tm])
   44.56        | _ => raise Same.SAME))
   44.57 -  |> Same.commit (Term_Subst.map_types_same unvarifyT_same)
   44.58 +  |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
   44.59    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   44.60  
   44.61  
    45.1 --- a/src/Pure/meta_simplifier.ML	Sat Mar 20 02:23:41 2010 +0100
    45.2 +++ b/src/Pure/meta_simplifier.ML	Sat Mar 20 17:33:11 2010 +0100
    45.3 @@ -612,8 +612,8 @@
    45.4    make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
    45.5      proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
    45.6  
    45.7 -(* FIXME avoid global thy and Logic.varify *)
    45.8 -fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
    45.9 +(* FIXME avoid global thy and Logic.varify_global *)
   45.10 +fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
   45.11  fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy);
   45.12  
   45.13  
    46.1 --- a/src/Pure/more_thm.ML	Sat Mar 20 02:23:41 2010 +0100
    46.2 +++ b/src/Pure/more_thm.ML	Sat Mar 20 17:33:11 2010 +0100
    46.3 @@ -59,7 +59,7 @@
    46.4      (ctyp * ctyp) list * (cterm * cterm) list
    46.5    val certify_instantiate:
    46.6      ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
    46.7 -  val unvarify: thm -> thm
    46.8 +  val unvarify_global: thm -> thm
    46.9    val close_derivation: thm -> thm
   46.10    val add_axiom: binding * term -> theory -> thm * theory
   46.11    val add_def: bool -> bool -> binding * term -> theory -> thm * theory
   46.12 @@ -295,12 +295,12 @@
   46.13    Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
   46.14  
   46.15  
   46.16 -(* unvarify: global schematic variables *)
   46.17 +(* unvarify_global: global schematic variables *)
   46.18  
   46.19 -fun unvarify th =
   46.20 +fun unvarify_global th =
   46.21    let
   46.22      val prop = Thm.full_prop_of th;
   46.23 -    val _ = map Logic.unvarify (prop :: Thm.hyps_of th)
   46.24 +    val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
   46.25        handle TERM (msg, _) => raise THM (msg, 0, [th]);
   46.26  
   46.27      val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
   46.28 @@ -326,7 +326,7 @@
   46.29    let
   46.30      val b' = if Binding.is_empty b then Binding.name ("axiom_" ^ serial_string ()) else b;
   46.31      val thy' = thy |> Theory.add_axioms_i [(b', prop)];
   46.32 -    val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b'));
   46.33 +    val axm = unvarify_global (Thm.axiom thy' (Sign.full_name thy' b'));
   46.34    in (axm, thy') end;
   46.35  
   46.36  fun add_def unchecked overloaded (b, prop) thy =
   46.37 @@ -334,12 +334,12 @@
   46.38      val tfrees = rev (map TFree (Term.add_tfrees prop []));
   46.39      val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
   46.40      val strip_sorts = tfrees ~~ tfrees';
   46.41 -    val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
   46.42 +    val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global)) (tfrees' ~~ tfrees);
   46.43  
   46.44      val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
   46.45      val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
   46.46      val axm' = Thm.axiom thy' (Sign.full_name thy' b);
   46.47 -    val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
   46.48 +    val thm = unvarify_global (Thm.instantiate (recover_sorts, []) axm');
   46.49    in (thm, thy') end;
   46.50  
   46.51  
    47.1 --- a/src/Pure/proofterm.ML	Sat Mar 20 02:23:41 2010 +0100
    47.2 +++ b/src/Pure/proofterm.ML	Sat Mar 20 17:33:11 2010 +0100
    47.3 @@ -827,7 +827,7 @@
    47.4  
    47.5  val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
    47.6    equal_elim_axm, abstract_rule_axm, combination_axm] =
    47.7 -    map (fn (s, t) => PAxm ("Pure." ^ s, varify t, NONE)) equality_axms;
    47.8 +    map (fn (s, t) => PAxm ("Pure." ^ s, varify_global t, NONE)) equality_axms;
    47.9  
   47.10  end;
   47.11  
    48.1 --- a/src/Pure/sign.ML	Sat Mar 20 02:23:41 2010 +0100
    48.2 +++ b/src/Pure/sign.ML	Sat Mar 20 17:33:11 2010 +0100
    48.3 @@ -441,7 +441,7 @@
    48.4          val c = full_name thy b;
    48.5          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    48.6            cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
    48.7 -        val T' = Logic.varifyT T;
    48.8 +        val T' = Logic.varifyT_global T;
    48.9        in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end;
   48.10      val args = map prep raw_args;
   48.11    in
   48.12 @@ -486,7 +486,7 @@
   48.13  fun add_const_constraint (c, opt_T) thy =
   48.14    let
   48.15      fun prepT raw_T =
   48.16 -      let val T = Logic.varifyT (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T)))
   48.17 +      let val T = Logic.varifyT_global (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T)))
   48.18        in cert_term thy (Const (c, T)); T end
   48.19        handle TYPE (msg, _, _) => error msg;
   48.20    in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end;
    49.1 --- a/src/Pure/theory.ML	Sat Mar 20 02:23:41 2010 +0100
    49.2 +++ b/src/Pure/theory.ML	Sat Mar 20 17:33:11 2010 +0100
    49.3 @@ -177,7 +177,7 @@
    49.4  
    49.5  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
    49.6    let
    49.7 -    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
    49.8 +    val axms = map (apsnd Logic.varify_global o prep_axm thy) raw_axms;
    49.9      val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
   49.10    in axioms' end);
   49.11  
   49.12 @@ -200,7 +200,7 @@
   49.13      val consts = Sign.consts_of thy;
   49.14      fun prep const =
   49.15        let val Const (c, T) = Sign.no_vars pp (Const const)
   49.16 -      in (c, Consts.typargs consts (c, Logic.varifyT T)) end;
   49.17 +      in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
   49.18  
   49.19      val lhs_vars = Term.add_tfreesT (#2 lhs) [];
   49.20      val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
   49.21 @@ -229,7 +229,7 @@
   49.22    let
   49.23      val declT = Sign.the_const_constraint thy c
   49.24        handle TYPE (msg, _, _) => error msg;
   49.25 -    val T' = Logic.varifyT T;
   49.26 +    val T' = Logic.varifyT_global T;
   49.27  
   49.28      fun message txt =
   49.29        [Pretty.block [Pretty.str "Specification of constant ",
    50.1 --- a/src/Pure/thm.ML	Sat Mar 20 02:23:41 2010 +0100
    50.2 +++ b/src/Pure/thm.ML	Sat Mar 20 17:33:11 2010 +0100
    50.3 @@ -137,8 +137,8 @@
    50.4    val map_tags: (Properties.T -> Properties.T) -> thm -> thm
    50.5    val norm_proof: thm -> thm
    50.6    val adjust_maxidx_thm: int -> thm -> thm
    50.7 -  val varifyT: thm -> thm
    50.8 -  val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
    50.9 +  val varifyT_global: thm -> thm
   50.10 +  val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   50.11    val freezeT: thm -> thm
   50.12    val assumption: int -> thm -> thm Seq.seq
   50.13    val eq_assumption: int -> thm -> thm
   50.14 @@ -1244,11 +1244,11 @@
   50.15    end;
   50.16  
   50.17  (* Replace all TFrees not fixed or in the hyps by new TVars *)
   50.18 -fun varifyT' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   50.19 +fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   50.20    let
   50.21      val tfrees = fold Term.add_tfrees hyps fixed;
   50.22      val prop1 = attach_tpairs tpairs prop;
   50.23 -    val (al, prop2) = Type.varify tfrees prop1;
   50.24 +    val (al, prop2) = Type.varify_global tfrees prop1;
   50.25      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   50.26    in
   50.27      (al, Thm (deriv_rule1 (Pt.varify_proof prop tfrees) der,
   50.28 @@ -1261,7 +1261,7 @@
   50.29        prop = prop3}))
   50.30    end;
   50.31  
   50.32 -val varifyT = #2 o varifyT' [];
   50.33 +val varifyT_global = #2 o varifyT_global' [];
   50.34  
   50.35  (* Replace all TVars by new TFrees *)
   50.36  fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
    51.1 --- a/src/Pure/type.ML	Sat Mar 20 02:23:41 2010 +0100
    51.2 +++ b/src/Pure/type.ML	Sat Mar 20 17:33:11 2010 +0100
    51.3 @@ -54,7 +54,7 @@
    51.4    (*special treatment of type vars*)
    51.5    val strip_sorts: typ -> typ
    51.6    val no_tvars: typ -> typ
    51.7 -  val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
    51.8 +  val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
    51.9    val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
   51.10    val legacy_freeze_type: typ -> typ
   51.11    val legacy_freeze_thaw: term -> term * (term -> term)
   51.12 @@ -284,9 +284,9 @@
   51.13        commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], []));
   51.14  
   51.15  
   51.16 -(* varify *)
   51.17 +(* varify_global *)
   51.18  
   51.19 -fun varify fixed t =
   51.20 +fun varify_global fixed t =
   51.21    let
   51.22      val fs = Term.fold_types (Term.fold_atyps
   51.23        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    52.1 --- a/src/Tools/Code/code_thingol.ML	Sat Mar 20 02:23:41 2010 +0100
    52.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Mar 20 17:33:11 2010 +0100
    52.3 @@ -613,7 +613,7 @@
    52.4        let
    52.5          val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
    52.6          val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
    52.7 -        val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
    52.8 +        val c_ty = (apsnd Logic.unvarifyT_global o dest_Const o snd
    52.9            o Logic.dest_equals o Thm.prop_of) thm;
   52.10        in
   52.11          ensure_const thy algbr eqngr c
    53.1 --- a/src/Tools/IsaPlanner/isand.ML	Sat Mar 20 02:23:41 2010 +0100
    53.2 +++ b/src/Tools/IsaPlanner/isand.ML	Sat Mar 20 17:33:11 2010 +0100
    53.3 @@ -213,7 +213,7 @@
    53.4      let 
    53.5        val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
    53.6        val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
    53.7 -    in #2 (Thm.varifyT' skiptfrees th) end;
    53.8 +    in #2 (Thm.varifyT_global' skiptfrees th) end;
    53.9  
   53.10  (* change schematic/meta vars to fresh free vars, avoiding name clashes 
   53.11     with "names" *)
    54.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Sat Mar 20 02:23:41 2010 +0100
    54.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Sat Mar 20 17:33:11 2010 +0100
    54.3 @@ -297,7 +297,7 @@
    54.4          |> Drule.implies_intr_list cprems
    54.5          |> Drule.forall_intr_list frees_of_fixed_vars
    54.6          |> Drule.forall_elim_list vars
    54.7 -        |> Thm.varifyT' othertfrees
    54.8 +        |> Thm.varifyT_global' othertfrees
    54.9          |-> K Drule.zero_var_indexes
   54.10      end;
   54.11  
    55.1 --- a/src/Tools/nbe.ML	Sat Mar 20 02:23:41 2010 +0100
    55.2 +++ b/src/Tools/nbe.ML	Sat Mar 20 17:33:11 2010 +0100
    55.3 @@ -102,12 +102,12 @@
    55.4            o apfst (fst o fst o dest_TVar) o Logic.dest_of_class) prem_props;
    55.5        in Drule.implies_elim_list thm prem_thms end;
    55.6    in ct
    55.7 -    |> Drule.cterm_rule Thm.varifyT
    55.8 +    |> Drule.cterm_rule Thm.varifyT_global
    55.9      |> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) =>
   55.10          (((v, 0), sort), TFree (v, sort'))) vs, []))
   55.11      |> Drule.cterm_rule Thm.freezeT
   55.12      |> conv
   55.13 -    |> Thm.varifyT
   55.14 +    |> Thm.varifyT_global
   55.15      |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
   55.16      |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
   55.17          (((v, 0), []), TVar ((v, 0), sort))) vs, [])