# HG changeset patch # User wenzelm # Date 1269102791 -3600 # Node ID e5980f0ad025e055f5b6add103b347d78d94bc0e # Parent 65258d2c32147112384d120b6032bc11a9d96043 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation; diff -r 65258d2c3214 -r e5980f0ad025 NEWS --- a/NEWS Sat Mar 20 02:23:41 2010 +0100 +++ b/NEWS Sat Mar 20 17:33:11 2010 +0100 @@ -290,6 +290,10 @@ Pretty.pp argument to merge, which is absent in the standard Theory_Data version. +* Renamed varify/unvarify operations to varify_global/unvarify_global +to emphasize that these only work in a global situation (which is +quite rare). + *** System *** diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Code_Evaluation.thy Sat Mar 20 17:33:11 2010 +0100 @@ -87,13 +87,14 @@ let val t = list_comb (Const (c, tys ---> ty), map Free (Name.names Name.context "a" tys)); - val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify) - (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t) + val (arg, rhs) = + pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) + (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t) val cty = Thm.ctyp_of thy ty; in @{thm term_of_anything} |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] - |> Thm.varifyT + |> Thm.varifyT_global end; fun add_term_of_code tyco raw_vs raw_cs thy = let @@ -131,7 +132,7 @@ in @{thm term_of_anything} |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs] - |> Thm.varifyT + |> Thm.varifyT_global end; fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy = let diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Sat Mar 20 17:33:11 2010 +0100 @@ -3438,7 +3438,7 @@ | mk_result prec NONE = @{term "UNIV :: real set"} fun realify t = let - val t = Logic.varify t + val t = Logic.varify_global t val m = map (fn (name, sort) => (name, @{typ real})) (Term.add_tvars t []) val t = Term.subst_TVars m t in t end diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Import/proof_kernel.ML Sat Mar 20 17:33:11 2010 +0100 @@ -1418,7 +1418,7 @@ val _ = message "INST_TYPE:" val _ = if_debug pth hth val tys_before = OldTerm.add_term_tfrees (prop_of th,[]) - val th1 = Thm.varifyT th + val th1 = Thm.varifyT_global th val tys_after = OldTerm.add_term_tvars (prop_of th1,[]) val tyinst = map (fn (bef, iS) => (case try (Lib.assoc (TFree bef)) lambda of @@ -2028,7 +2028,7 @@ names' (thy1,th) val _ = ImportRecorder.add_specification names' th - val res' = Thm.unvarify res + val res' = Thm.unvarify_global res val hth = HOLThm(rens,res') val rew = rewrite_hol4_term (concl_of res') thy' val th = equal_elim rew res' diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Import/shuffler.ML Sat Mar 20 17:33:11 2010 +0100 @@ -265,7 +265,7 @@ let val cU = ctyp_of thy U val tfrees = OldTerm.add_term_tfrees (prop_of thm,[]) - val (rens, thm') = Thm.varifyT' + val (rens, thm') = Thm.varifyT_global' (remove (op = o apsnd fst) name tfrees) thm val mid = case rens of @@ -592,7 +592,7 @@ fun process [] = NONE | process ((name,th)::thms) = let - val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th))) + val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th))) val triv_th = trivial rhs val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th)) val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Mutabelle/mutabelle.ML Sat Mar 20 17:33:11 2010 +0100 @@ -218,7 +218,7 @@ val typeSignature = #tsig (Sign.rep_sg consSig) in if ((consNameStr = forbNameStr) - andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT forbType)))) + andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT_global forbType)))) then true else in_list_forb consSig (consNameStr,consType) xs end; diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Mar 20 17:33:11 2010 +0100 @@ -849,7 +849,7 @@ fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th => let - val _ $ (_ $ (Rep $ x)) = Logic.unvarify (prop_of th); + val _ $ (_ $ (Rep $ x)) = Logic.unvarify_global (prop_of th); val Type ("fun", [T, U]) = fastype_of Rep; val permT = mk_permT (Type (atom, [])); val pi = Free ("pi", permT); @@ -1394,7 +1394,7 @@ (pnames ~~ map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct_aux)))) @ map (fn (_, f) => - let val f' = Logic.varify f + let val f' = Logic.varify_global f in (cterm_of thy9 f', cterm_of thy9 (Const ("Nominal.supp", fastype_of f'))) end) fresh_fs) induct_aux; @@ -1677,14 +1677,14 @@ val induct_aux_rec = Drule.cterm_instantiate (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort)) - (map (fn (aT, f) => (Logic.varify f, Abs ("z", HOLogic.unitT, + (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT, Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple))) fresh_fs @ map (fn (((P, T), (x, U)), Q) => - (Var ((P, 0), Logic.varifyT (fsT' --> T --> HOLogic.boolT)), + (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)), Abs ("z", HOLogic.unitT, absfree (x, U, Q)))) (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @ - map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T))) + map (fn (s, T) => (Var ((s, 0), Logic.varifyT_global T), Free (s, T))) rec_unique_frees)) induct_aux; fun obtain_fresh_name vs ths rec_fin_supp T (freshs1, freshs2, ctxt) = diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/SMT/Tools/smt_translate.ML --- a/src/HOL/SMT/Tools/smt_translate.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/SMT/Tools/smt_translate.ML Sat Mar 20 17:33:11 2010 +0100 @@ -126,11 +126,11 @@ let fun dest (t, bn) = let val (n, T) = Term.dest_Const t - in (n, (Logic.varifyT T, K (SOME o pair bn))) end + in (n, (Logic.varifyT_global T, K (SOME o pair bn))) end in Symtab.make (AList.group (op =) (map dest entries)) end fun builtin_add (t, f) tab = - let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t) + let val (n, T) = apsnd Logic.varifyT_global (Term.dest_Const t) in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end fun builtin_lookup tab thy (n, T) ts = diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Sat Mar 20 17:33:11 2010 +0100 @@ -46,7 +46,7 @@ in SOME {case_name = case_name, constructors = map (fn (cname, dts') => - Const (cname, Logic.varifyT (map mk_ty dts' ---> T))) constrs} + Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs} end | NONE => NONE; @@ -87,7 +87,7 @@ val (_, Ty) = dest_Const c val Ts = binder_types Ty; val names = Name.variant_list used - (Datatype_Prop.make_tnames (map Logic.unvarifyT Ts)); + (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)); val ty = body_type Ty; val ty_theta = ty_match ty colty handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1) diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Sat Mar 20 17:33:11 2010 +0100 @@ -310,7 +310,7 @@ (#case_rewrites o Datatype_Data.the_info thy) tyco; val thms as hd_thm :: _ = raw_thms |> Conjunction.intr_balanced - |> Thm.unvarify + |> Thm.unvarify_global |> Conjunction.elim_balanced (length raw_thms) |> map Simpdata.mk_meta_eq |> map Drule.zero_var_indexes @@ -332,7 +332,7 @@ |> Thm.implies_intr asm |> Thm.generalize ([], params) 0 |> AxClass.unoverload thy - |> Thm.varifyT + |> Thm.varifyT_global end; diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Mar 20 17:33:11 2010 +0100 @@ -128,7 +128,7 @@ (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm) ||> Sign.restore_naming thy; - val ivs = rev (Term.add_vars (Logic.varify (Datatype_Prop.make_ind [descr] sorts)) []); + val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []); val rvs = rev (Thm.fold_terms Term.add_vars thm' []); val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *) tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs); @@ -139,7 +139,7 @@ (fold_rev (fn (f, p) => fn prf => (case head_of (strip_abs_body f) of Free (s, T) => - let val T' = Logic.varifyT T + let val T' = Logic.varifyT_global T in Abst (s, SOME T', Proofterm.prf_abstract_over (Var ((s, 0), T')) (AbsP ("H", SOME p, prf))) end @@ -149,8 +149,8 @@ val r' = if null is then r - else Logic.varify (fold_rev lambda - (map Logic.unvarify ivs1 @ filter_out is_unit + else Logic.varify_global (fold_rev lambda + (map Logic.unvarify_global ivs1 @ filter_out is_unit (map (head_of o strip_abs_body) rec_fns)) r); in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end; @@ -179,7 +179,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), Logic.varifyT T); + val y = Var (("y", 0), Logic.varifyT_global T); val y' = Free ("y", T); val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems, @@ -200,10 +200,10 @@ val P = Var (("P", 0), rT' --> HOLogic.boolT); val prf = forall_intr_prf (y, forall_intr_prf (P, fold_rev (fn (p, r) => fn prf => - forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), prf))) + forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf))) (prems ~~ rs) (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))))); - val r' = Logic.varify (Abs ("y", T, + val r' = Logic.varify_global (Abs ("y", T, list_abs (map dest_Free rs, list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))); diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 20 17:33:11 2010 +0100 @@ -566,7 +566,7 @@ SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac}, set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \ Frac"} - |> Logic.varify, + |> Logic.varify_global, set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE} else case Typedef.get_info_global thy s of (* FIXME handle multiple typedef interpretations (!??) *) @@ -599,7 +599,7 @@ handle Type.TYPE_MATCH => raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) fun varify_and_instantiate_type thy T1 T1' T2 = - instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2) + instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2) (* theory -> typ -> typ -> styp *) fun repair_constr_type thy body_T' T = diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Mar 20 17:33:11 2010 +0100 @@ -326,7 +326,7 @@ (* theory -> typ * typ -> bool *) fun varified_type_match thy (candid_T, pat_T) = - strict_type_match thy (candid_T, Logic.varifyT pat_T) + strict_type_match thy (candid_T, Logic.varifyT_global pat_T) (* atom_pool -> (string * string) * (string * string) -> scope -> nut list -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Mar 20 17:33:11 2010 +0100 @@ -404,7 +404,7 @@ (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)) (#2 (Type.varify [] t)) + let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t)) in (maxidx_of_term t', t'::ts) end; val (i, cs') = List.foldr varify (~1, []) cs; val (i', intr_ts') = List.foldr varify (i, []) intr_ts; diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sat Mar 20 17:33:11 2010 +0100 @@ -87,7 +87,7 @@ (* theory -> term -> (string list, term list list) *) fun dest_code_eqn eqn = let - val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn)) + val (lhs, rhs) = Logic.dest_equals (Logic.unvarify_global (Thm.prop_of eqn)) val (func, args) = strip_comb lhs in ((func, args), rhs) end; @@ -372,7 +372,7 @@ *) val thy'' = Fun_Pred.map - (fold Item_Net.update (map (apfst Logic.varify) + (fold Item_Net.update (map (apfst Logic.varify_global) (distinct (op =) funs ~~ (#preds ind_result)))) thy' (*val _ = print_specs thy'' specs*) in @@ -397,7 +397,7 @@ | lookup_pred _ = NONE *) fun lookup_pred t = lookup thy (Fun_Pred.get thy) t - val intro_t = (Logic.unvarify o prop_of) intro + val intro_t = Logic.unvarify_global (prop_of intro) val (prems, concl) = Logic.strip_horn intro_t val frees = map fst (Term.add_frees intro_t []) fun rewrite prem names = diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Mar 20 17:33:11 2010 +0100 @@ -313,7 +313,7 @@ fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) = let val vars = map Var (Term.add_vars abs_arg []) - val abs_arg' = Logic.unvarify abs_arg + val abs_arg' = Logic.unvarify_global abs_arg val frees = map Free (Term.add_frees abs_arg' []) val constname = Name.variant (map (Long_Name.base_name o fst) new_defs) ((Long_Name.base_name constname) ^ "_hoaux") @@ -326,7 +326,8 @@ |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])] in - (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy')) + (list_comb (Logic.varify_global const, vars), + ((full_constname, [definition])::new_defs, thy')) end | replace_abs_arg arg (new_defs, thy) = if (is_predT (fastype_of arg)) then diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Mar 20 17:33:11 2010 +0100 @@ -267,7 +267,7 @@ in Goal.prove_internal [ex_tm] conc tacf |> forall_intr_list frees |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) - |> Thm.varifyT + |> Thm.varifyT_global end; diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/choice_specification.ML Sat Mar 20 17:33:11 2010 +0100 @@ -90,9 +90,9 @@ | collect_consts (tm as Const _,tms) = insert (op aconv) tm tms | collect_consts ( _,tms) = tms -(* Complementing Type.varify... *) +(* Complementing Type.varify_global... *) -fun unvarify t fmap = +fun unvarify_global t fmap = let val fmap' = map Library.swap fmap fun unthaw (f as (a, S)) = @@ -135,7 +135,7 @@ val prop = myfoldr HOLogic.mk_conj (map fst props'') val cprop = cterm_of thy (HOLogic.mk_Trueprop prop) - val (vmap, prop_thawed) = Type.varify [] prop + val (vmap, prop_thawed) = Type.varify_global [] prop val thawed_prop_consts = collect_consts (prop_thawed,[]) val (altcos,overloaded) = Library.split_list cos val (names,sconsts) = Library.split_list altcos @@ -145,14 +145,14 @@ fun proc_const c = let - val (_, c') = Type.varify [] c + val (_, c') = Type.varify_global [] c val (cname,ctyp) = dest_Const c' in case filter (fn t => let val (name,typ) = dest_Const t in name = cname andalso Sign.typ_equiv thy (typ, ctyp) end) thawed_prop_consts of [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found") - | [cf] => unvarify cf vmap + | [cf] => unvarify_global cf vmap | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)") end val proc_consts = map proc_const consts diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Sat Mar 20 17:33:11 2010 +0100 @@ -70,9 +70,9 @@ val params = map dest_Var (take nparms ts); val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs)); fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)), - map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @ + map (Logic.unvarifyT_global o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @ filter_out (equal Extraction.nullT) (map - (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), + (Logic.unvarifyT_global 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) @@ -339,13 +339,13 @@ let val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)); val s' = Long_Name.base_name s; - val T' = Logic.unvarifyT T; + val T' = Logic.unvarifyT_global T; in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) |> distinct (op = o pairself (#1 o #1)) |> map (apfst (apfst (apfst Binding.name))) |> split_list; - val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T)) + val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT_global T)) (List.take (snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms)); @@ -357,7 +357,7 @@ no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} rlzpreds rlzparams (map (fn (rintr, intr) => ((Binding.name (Long_Name.base_name (name_of_thm intr)), []), - subst_atomic rlzpreds' (Logic.unvarify rintr))) + subst_atomic rlzpreds' (Logic.unvarify_global rintr))) (rintrs ~~ maps snd rss)) [] ||> Sign.root_path; val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3'; @@ -383,7 +383,7 @@ (used @ rnames) (replicate (length intrs) "s"); val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) => let - val (P, Q) = strip_one name (Logic.unvarify rlz); + val (P, Q) = strip_one name (Logic.unvarify_global rlz); val Q' = strip_all' [] rnames' Q in (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q') @@ -446,7 +446,7 @@ map reorder2 (intrs ~~ (length prems - 1 downto 0)) @ [Bound (length prems)])); val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim); - val rlz' = strip_all (Logic.unvarify rlz); + val rlz' = strip_all (Logic.unvarify_global rlz); val rews = map mk_meta_eq case_thms; val thm = Goal.prove_global thy [] (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/meson.ML Sat Mar 20 17:33:11 2010 +0100 @@ -667,7 +667,7 @@ fun make_meta_clause th = let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th in - (zero_var_indexes o Thm.varifyT o thaw 0 o + (zero_var_indexes o Thm.varifyT_global o thaw 0 o negated_asm_of_head o make_horn resolution_clause_rules) fth end; diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/old_primrec.ML Sat Mar 20 17:33:11 2010 +0100 @@ -35,7 +35,7 @@ fun unify_consts thy cs intr_ts = (let fun varify t (i, ts) = - let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t)) + let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify_global [] t)) in (maxidx_of_term t', t'::ts) end; val (i, cs') = fold_rev varify cs (~1, []); val (i', intr_ts') = fold_rev varify intr_ts (i, []); @@ -281,7 +281,7 @@ thy' |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps); val simps'' = maps snd simps'; - val lhss = map (Logic.varify o fst o Logic.dest_equals o snd) defs'; + val lhss = map (Logic.varify_global o fst o Logic.dest_equals o snd) defs'; in thy'' |> note (("simps", diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/quickcheck_generators.ML Sat Mar 20 17:33:11 2010 +0100 @@ -316,7 +316,7 @@ fun perhaps_constrain thy insts raw_vs = let fun meet_random (T, sort) = Sorts.meet_sort (Sign.classes_of thy) - (Logic.varifyT T, sort); + (Logic.varifyT_global T, sort); val vtab = Vartab.empty |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs |> fold meet_random insts; diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Sat Mar 20 17:33:11 2010 +0100 @@ -16,7 +16,7 @@ open Proofterm; val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o - Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT) + Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT) (** eliminate meta-equality rules **) diff -r 65258d2c3214 -r e5980f0ad025 src/HOL/Tools/typecopy.ML --- a/src/HOL/Tools/typecopy.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/HOL/Tools/typecopy.ML Sat Mar 20 17:33:11 2010 +0100 @@ -61,7 +61,7 @@ let val exists_thm = UNIV_I - |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] []; + |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] []; val inject' = inject OF [exists_thm, exists_thm]; val proj_def = inverse OF [exists_thm]; val info = { @@ -95,7 +95,7 @@ typ = ty_rep, ... } = get_info thy tyco; (* FIXME handle multiple typedef interpretations (!??) *) val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco; - val constr = (c, Logic.unvarifyT (Sign.the_const_type thy c)); + val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c)); val ty = Type (tyco, map TFree vs); val proj = Const (proj, ty --> ty_rep); val (t_x, t_y) = (Free ("x", ty), Free ("y", ty)); @@ -109,7 +109,7 @@ THEN ALLGOALS (rtac @{thm refl}); fun mk_eq_refl thy = @{thm HOL.eq_refl} |> Thm.instantiate - ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []) + ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], []) |> AxClass.unoverload thy; in thy diff -r 65258d2c3214 -r e5980f0ad025 src/Provers/Arith/abel_cancel.ML --- a/src/Provers/Arith/abel_cancel.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Provers/Arith/abel_cancel.ML Sat Mar 20 17:33:11 2010 +0100 @@ -88,7 +88,7 @@ val sum_conv = Simplifier.mk_simproc "cancel_sums" - (map (Drule.cterm_fun Logic.varify) Data.sum_pats) (K sum_proc); + (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc); (*A simproc to cancel like terms on the opposite sides of relations: diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Isar/class.ML Sat Mar 20 17:33:11 2010 +0100 @@ -257,7 +257,7 @@ | t => t); val raw_pred = Locale.intros_of thy class |> fst - |> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of); + |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); fun get_axiom thy = case (#axioms o AxClass.get_info thy) class of [] => NONE | [thm] => SOME thm; diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Isar/class_target.ML Sat Mar 20 17:33:11 2010 +0100 @@ -332,7 +332,7 @@ |> Sign.declare_const ((b, Type.strip_sorts ty'), mx) |> snd |> Thm.add_def false false (b_def, def_eq) - |>> Thm.varifyT + |>> Thm.varifyT_global |-> (fn def_thm => PureThy.store_thm (b_def, def_thm) #> snd #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) @@ -347,7 +347,7 @@ val c' = Sign.full_name thy b; val rhs' = Pattern.rewrite_term thy unchecks [] rhs; val ty' = Term.fastype_of rhs'; - val rhs'' = map_types Logic.varifyT rhs'; + val rhs'' = map_types Logic.varifyT_global rhs'; in thy |> Sign.add_abbrev (#1 prmode) (b, rhs'') @@ -530,7 +530,7 @@ val (tycos, vs, sort) = (#arities o the_instantiation) lthy; val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; fun after_qed' results = - Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT) results) + Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) #> after_qed; in lthy diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Isar/code.ML Sat Mar 20 17:33:11 2010 +0100 @@ -337,7 +337,7 @@ (Binding.qualified_name tyco, n) | _ => I) decls end; -fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars; +fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars; fun read_signature thy = cert_signature thy o Type.strip_sorts o Syntax.parse_typ (ProofContext.init thy); @@ -374,7 +374,7 @@ let val _ = Thm.cterm_of thy (Const (c, raw_ty)); val ty = subst_signature thy c raw_ty; - val ty_decl = (Logic.unvarifyT o const_typ thy) c; + val ty_decl = (Logic.unvarifyT_global o const_typ thy) c; fun last_typ c_ty ty = let val tfrees = Term.add_tfreesT ty []; @@ -684,7 +684,7 @@ (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) mapping v))); in thm - |> Thm.varifyT + |> Thm.varifyT_global |> Thm.certify_instantiate (inst, []) |> pair subst end; @@ -697,7 +697,7 @@ val ty_abs = (fastype_of o snd o dest_comb) lhs; val abs = Thm.cterm_of thy (Const (c, ty --> ty_abs)); val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm]; - in (c, (Thm.varifyT o zero_var_indexes) raw_concrete_thm) end; + in (c, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end; fun add_rhss_of_eqn thy t = let @@ -706,7 +706,8 @@ | add_const _ = I in fold_aterms add_const t end; -fun dest_eqn thy = apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy o Logic.unvarify; +fun dest_eqn thy = + apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy o Logic.unvarify_global; abstype cert = Equations of thm * bool list | Projection of term * string @@ -811,14 +812,14 @@ val thms = if null propers then [] else cert_thm |> Local_Defs.expand [snd (get_head thy cert_thm)] - |> Thm.varifyT + |> Thm.varifyT_global |> Conjunction.elim_balanced (length propers); in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end | equations_of_cert thy (Projection (t, tyco)) = let val (_, ((abs, _), _)) = get_abstype_spec thy tyco; val tyscm = typscheme_projection thy t; - val t' = map_types Logic.varifyT t; + val t' = map_types Logic.varifyT_global t; in (tyscm, [((SOME abs, dest_eqn thy t'), (NONE, true))]) end | equations_of_cert thy (Abstract (abs_thm, tyco)) = let @@ -827,22 +828,24 @@ val _ = fold_aterms (fn Const (c, _) => if c = abs then error ("Abstraction violation in abstract code equation\n" ^ Display.string_of_thm_global thy abs_thm) else I | _ => I) (Thm.prop_of abs_thm); - in (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT abs_thm), true))]) end; + in + (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT_global abs_thm), true))]) + end; fun pretty_cert thy (cert as Equations _) = (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd) o snd o equations_of_cert thy) cert | pretty_cert thy (Projection (t, _)) = - [Syntax.pretty_term_global thy (map_types Logic.varifyT t)] + [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)] | pretty_cert thy (Abstract (abs_thm, tyco)) = - [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT) abs_thm]; + [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm]; fun bare_thms_of_cert thy (cert as Equations _) = (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) o snd o equations_of_cert thy) cert | bare_thms_of_cert thy (Projection _) = [] | bare_thms_of_cert thy (Abstract (abs_thm, tyco)) = - [Thm.varifyT (snd (concretify_abs thy tyco abs_thm))]; + [Thm.varifyT_global (snd (concretify_abs thy tyco abs_thm))]; end; @@ -1157,7 +1160,7 @@ (del_eqns abs #> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert)))) #> change_fun_spec false rep ((K o Proj) - (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco)) + (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco)) #> Abstype_Interpretation.data (tyco, serial ())); in thy diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Isar/constdefs.ML Sat Mar 20 17:33:11 2010 +0100 @@ -56,7 +56,7 @@ |> Sign.add_consts_i [(b, T, mx)] |> PureThy.add_defs false [((name, def), atts)] |-> (fn [thm] => (* FIXME thm vs. atts !? *) - Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #> + Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify_global head], [thm]) #> Code.add_default_eqn thm); in ((c, T), thy') end; diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Isar/expression.ML Sat Mar 20 17:33:11 2010 +0100 @@ -162,7 +162,7 @@ val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst; (* type inference and contexts *) - val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types; + val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT_global) parm_types; val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar); val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts'; val res = Syntax.check_terms ctxt arg; @@ -346,7 +346,7 @@ val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list; val inst' = prep_inst ctxt parm_names inst; val parm_types' = map (TypeInfer.paramify_vars o - Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types; + Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types; val inst'' = map2 TypeInfer.constrain parm_types' inst'; val insts' = insts @ [(loc, (prfx, inst''))]; val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt; diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Isar/obtain.ML Sat Mar 20 17:33:11 2010 +0100 @@ -197,7 +197,7 @@ val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule; val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt; - val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule'; + val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule'; val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt'; val (prems, ctxt'') = Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params)) @@ -252,7 +252,7 @@ val vars' = map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ (map snd vars @ replicate (length ys) NoSyn); - val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule'; + val rule'' = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule'; in ((vars', rule''), ctxt') end; fun inferred_type (binding, _, mx) ctxt = diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Isar/theory_target.ML Sat Mar 20 17:33:11 2010 +0100 @@ -227,7 +227,7 @@ (if is_locale then Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs)) #-> (fn (lhs, _) => - let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in + let val lhs' = Term.list_comb (Logic.unvarify_global lhs, xs) in syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t')) end) diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Proof/extraction.ML Sat Mar 20 17:33:11 2010 +0100 @@ -206,7 +206,7 @@ fun read_condeq thy = let val thy' = add_syntax thy in fn s => - let val t = Logic.varify (Syntax.read_prop_global thy' s) + let val t = Logic.varify_global (Syntax.read_prop_global thy' s) in (map Logic.dest_equals (Logic.strip_imp_prems t), Logic.dest_equals (Logic.strip_imp_concl t)) @@ -732,7 +732,7 @@ in thy' |> PureThy.store_thm (Binding.qualified_name (corr_name s vs), - Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop)) + Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop)) (Thm.forall_elim_var 0) (forall_intr_frees (ProofChecker.thm_of_proof thy' (fst (Proofterm.freeze_thaw_prf prf)))))) diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Sat Mar 20 17:33:11 2010 +0100 @@ -217,7 +217,7 @@ fun read_proof thy = let val rd = read_term thy proofT - in fn ty => fn s => proof_of_term thy ty (Logic.varify (rd s)) end; + in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; fun proof_syntax prf = let diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Proof/proofchecker.ML Sat Mar 20 17:33:11 2010 +0100 @@ -36,7 +36,7 @@ fun thm_of_atom thm Ts = let val tvars = OldTerm.term_tvars (Thm.full_prop_of thm); - val (fmap, thm') = Thm.varifyT' [] thm; + val (fmap, thm') = Thm.varifyT_global' [] thm; val ctye = map (pairself (Thm.ctyp_of thy)) (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) in diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Tools/find_consts.ML Sat Mar 20 17:33:11 2010 +0100 @@ -68,7 +68,7 @@ fun pretty_const ctxt (nm, ty) = let - val ty' = Logic.unvarifyT ty; + val ty' = Logic.unvarifyT_global ty; in Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk, diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/axclass.ML Sat Mar 20 17:33:11 2010 +0100 @@ -309,7 +309,7 @@ |-> (fn const' as Const (c'', _) => Thm.add_def false true (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const')) - #>> Thm.varifyT + #>> Thm.varifyT_global #-> (fn thm => add_inst_param (c, tyco) (c'', thm) #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), []) #> snd diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/codegen.ML Sat Mar 20 17:33:11 2010 +0100 @@ -474,7 +474,7 @@ (**** retrieve definition of constant ****) fun is_instance T1 T2 = - Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT T2); + Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT_global T2); fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) => s = s' andalso is_instance T T') (#consts (CodegenData.get thy))); diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/conjunction.ML Sat Mar 20 17:33:11 2010 +0100 @@ -75,7 +75,8 @@ val A_B = read_prop "A &&& B"; val conjunction_def = - Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def"); + Thm.unvarify_global + (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def"); fun conjunctionD which = Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/defs.ML --- a/src/Pure/defs.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/defs.ML Sat Mar 20 17:33:11 2010 +0100 @@ -34,7 +34,7 @@ let val prt_args = if null args then [] - else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT) args)]; + else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT_global) args)]; in Pretty.block (Pretty.str c :: prt_args) end; fun plain_args args = diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/display.ML --- a/src/Pure/display.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/display.ML Sat Mar 20 17:33:11 2010 +0100 @@ -131,9 +131,9 @@ fun prt_sort S = Syntax.pretty_sort ctxt S; fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]); fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); - val prt_typ_no_tvars = prt_typ o Logic.unvarifyT; + val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); - val prt_term_no_vars = prt_term o Logic.unvarify; + val prt_term_no_vars = prt_term o Logic.unvarify_global; fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; val prt_const' = Defs.pretty_const (Syntax.pp ctxt); diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/drule.ML --- a/src/Pure/drule.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/drule.ML Sat Mar 20 17:33:11 2010 +0100 @@ -312,7 +312,7 @@ Thm.forall_elim_vars (maxidx + 1) #> Thm.strip_shyps #> zero_var_indexes - #> Thm.varifyT); + #> Thm.varifyT_global); val export_without_context = flexflex_unique @@ -691,7 +691,7 @@ local val A = certify (Free ("A", propT)); - val axiom = Thm.unvarify o Thm.axiom (Context.the_theory (Context.the_thread_data ())); + val axiom = Thm.unvarify_global o Thm.axiom (Context.the_theory (Context.the_thread_data ())); val prop_def = axiom "Pure.prop_def"; val term_def = axiom "Pure.term_def"; val sort_constraint_def = axiom "Pure.sort_constraint_def"; @@ -762,7 +762,8 @@ val sort_constraint_eq = store_standard_thm (Binding.conceal (Binding.name "sort_constraint_eq")) (Thm.equal_intr - (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI))) + (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) + (Thm.unvarify_global sort_constraintI))) (implies_intr_list [A, C] (Thm.assume A))); end; diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/goal.ML --- a/src/Pure/goal.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/goal.ML Sat Mar 20 17:33:11 2010 +0100 @@ -129,7 +129,8 @@ val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees; val global_prop = - cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)))) + cert (Term.map_types Logic.varifyT_global + (fold_rev Logic.all xs (Logic.list_implies (As, prop)))) |> Thm.weaken_sorts (Variable.sorts_of ctxt); val global_result = result |> Future.map (Drule.flexflex_unique #> diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/logic.ML --- a/src/Pure/logic.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/logic.ML Sat Mar 20 17:33:11 2010 +0100 @@ -68,10 +68,10 @@ val list_rename_params: string list * term -> term val assum_pairs: int * term -> (term*term)list val assum_problems: int * term -> (term -> term) * term list * term - val varifyT: typ -> typ - val unvarifyT: typ -> typ - val varify: term -> term - val unvarify: term -> term + val varifyT_global: typ -> typ + val unvarifyT_global: typ -> typ + val varify_global: term -> term + val unvarify_global: term -> term val get_goal: term -> int -> term val goal_params: term -> int -> term * term list val prems_of_goal: term -> int -> term list @@ -465,35 +465,35 @@ fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi); fun bad_fixed x = "Illegal fixed variable: " ^ quote x; -fun varifyT_same ty = ty +fun varifyT_global_same ty = ty |> Term_Subst.map_atypsT_same (fn TFree (a, S) => TVar ((a, 0), S) | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])); -fun unvarifyT_same ty = ty +fun unvarifyT_global_same ty = ty |> Term_Subst.map_atypsT_same (fn TVar ((a, 0), S) => TFree (a, S) | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []) | TFree (a, _) => raise TYPE (bad_fixed a, [ty], [])); -val varifyT = Same.commit varifyT_same; -val unvarifyT = Same.commit unvarifyT_same; +val varifyT_global = Same.commit varifyT_global_same; +val unvarifyT_global = Same.commit unvarifyT_global_same; -fun varify tm = tm +fun varify_global tm = tm |> Same.commit (Term_Subst.map_aterms_same (fn Free (x, T) => Var ((x, 0), T) | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) | _ => raise Same.SAME)) - |> Same.commit (Term_Subst.map_types_same varifyT_same) + |> Same.commit (Term_Subst.map_types_same varifyT_global_same) handle TYPE (msg, _, _) => raise TERM (msg, [tm]); -fun unvarify tm = tm +fun unvarify_global tm = tm |> Same.commit (Term_Subst.map_aterms_same (fn Var ((x, 0), T) => Free (x, T) | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) | Free (x, _) => raise TERM (bad_fixed x, [tm]) | _ => raise Same.SAME)) - |> Same.commit (Term_Subst.map_types_same unvarifyT_same) + |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same) handle TYPE (msg, _, _) => raise TERM (msg, [tm]); diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/meta_simplifier.ML Sat Mar 20 17:33:11 2010 +0100 @@ -612,8 +612,8 @@ make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct => proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []}; -(* FIXME avoid global thy and Logic.varify *) -fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify); +(* FIXME avoid global thy and Logic.varify_global *) +fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global); fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy); diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/more_thm.ML Sat Mar 20 17:33:11 2010 +0100 @@ -59,7 +59,7 @@ (ctyp * ctyp) list * (cterm * cterm) list val certify_instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm - val unvarify: thm -> thm + val unvarify_global: thm -> thm val close_derivation: thm -> thm val add_axiom: binding * term -> theory -> thm * theory val add_def: bool -> bool -> binding * term -> theory -> thm * theory @@ -295,12 +295,12 @@ Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th; -(* unvarify: global schematic variables *) +(* unvarify_global: global schematic variables *) -fun unvarify th = +fun unvarify_global th = let val prop = Thm.full_prop_of th; - val _ = map Logic.unvarify (prop :: Thm.hyps_of th) + val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) handle TERM (msg, _) => raise THM (msg, 0, [th]); val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); @@ -326,7 +326,7 @@ let val b' = if Binding.is_empty b then Binding.name ("axiom_" ^ serial_string ()) else b; val thy' = thy |> Theory.add_axioms_i [(b', prop)]; - val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b')); + val axm = unvarify_global (Thm.axiom thy' (Sign.full_name thy' b')); in (axm, thy') end; fun add_def unchecked overloaded (b, prop) thy = @@ -334,12 +334,12 @@ val tfrees = rev (map TFree (Term.add_tfrees prop [])); val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees)); val strip_sorts = tfrees ~~ tfrees'; - val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees); + val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global)) (tfrees' ~~ tfrees); val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop; val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy; val axm' = Thm.axiom thy' (Sign.full_name thy' b); - val thm = unvarify (Thm.instantiate (recover_sorts, []) axm'); + val thm = unvarify_global (Thm.instantiate (recover_sorts, []) axm'); in (thm, thy') end; diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/proofterm.ML Sat Mar 20 17:33:11 2010 +0100 @@ -827,7 +827,7 @@ val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, equal_elim_axm, abstract_rule_axm, combination_axm] = - map (fn (s, t) => PAxm ("Pure." ^ s, varify t, NONE)) equality_axms; + map (fn (s, t) => PAxm ("Pure." ^ s, varify_global t, NONE)) equality_axms; end; diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/sign.ML --- a/src/Pure/sign.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/sign.ML Sat Mar 20 17:33:11 2010 +0100 @@ -441,7 +441,7 @@ val c = full_name thy b; val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b)); - val T' = Logic.varifyT T; + val T' = Logic.varifyT_global T; in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end; val args = map prep raw_args; in @@ -486,7 +486,7 @@ fun add_const_constraint (c, opt_T) thy = let fun prepT raw_T = - let val T = Logic.varifyT (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T))) + let val T = Logic.varifyT_global (Type.no_tvars (Term.no_dummyT (certify_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; diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/theory.ML --- a/src/Pure/theory.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/theory.ML Sat Mar 20 17:33:11 2010 +0100 @@ -177,7 +177,7 @@ fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms => let - val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms; + val axms = map (apsnd Logic.varify_global o prep_axm thy) raw_axms; val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms; in axioms' end); @@ -200,7 +200,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, Logic.varifyT T)) end; + in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end; val lhs_vars = Term.add_tfreesT (#2 lhs) []; val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v => @@ -229,7 +229,7 @@ let val declT = Sign.the_const_constraint thy c handle TYPE (msg, _, _) => error msg; - val T' = Logic.varifyT T; + val T' = Logic.varifyT_global T; fun message txt = [Pretty.block [Pretty.str "Specification of constant ", diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/thm.ML Sat Mar 20 17:33:11 2010 +0100 @@ -137,8 +137,8 @@ val map_tags: (Properties.T -> Properties.T) -> thm -> thm val norm_proof: thm -> thm val adjust_maxidx_thm: int -> thm -> thm - val varifyT: thm -> thm - val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm + val varifyT_global: thm -> thm + val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm val freezeT: thm -> thm val assumption: int -> thm -> thm Seq.seq val eq_assumption: int -> thm -> thm @@ -1244,11 +1244,11 @@ end; (* Replace all TFrees not fixed or in the hyps by new TVars *) -fun varifyT' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = +fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = let val tfrees = fold Term.add_tfrees hyps fixed; val prop1 = attach_tpairs tpairs prop; - val (al, prop2) = Type.varify tfrees prop1; + val (al, prop2) = Type.varify_global tfrees prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in (al, Thm (deriv_rule1 (Pt.varify_proof prop tfrees) der, @@ -1261,7 +1261,7 @@ prop = prop3})) end; -val varifyT = #2 o varifyT' []; +val varifyT_global = #2 o varifyT_global' []; (* Replace all TVars by new TFrees *) fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) = diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/type.ML --- a/src/Pure/type.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/type.ML Sat Mar 20 17:33:11 2010 +0100 @@ -54,7 +54,7 @@ (*special treatment of type vars*) val strip_sorts: typ -> typ val no_tvars: typ -> typ - val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term + val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term val legacy_freeze_thaw_type: typ -> typ * (typ -> typ) val legacy_freeze_type: typ -> typ val legacy_freeze_thaw: term -> term * (term -> term) @@ -284,9 +284,9 @@ commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], [])); -(* varify *) +(* varify_global *) -fun varify fixed t = +fun varify_global 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 []; diff -r 65258d2c3214 -r e5980f0ad025 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Tools/Code/code_thingol.ML Sat Mar 20 17:33:11 2010 +0100 @@ -613,7 +613,7 @@ let val c_inst = Const (c, map_type_tfree (K arity_typ') ty); val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst); - val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd + val c_ty = (apsnd Logic.unvarifyT_global o dest_Const o snd o Logic.dest_equals o Thm.prop_of) thm; in ensure_const thy algbr eqngr c diff -r 65258d2c3214 -r e5980f0ad025 src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Tools/IsaPlanner/isand.ML Sat Mar 20 17:33:11 2010 +0100 @@ -213,7 +213,7 @@ let val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[])); - in #2 (Thm.varifyT' skiptfrees th) end; + in #2 (Thm.varifyT_global' skiptfrees th) end; (* change schematic/meta vars to fresh free vars, avoiding name clashes with "names" *) diff -r 65258d2c3214 -r e5980f0ad025 src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Tools/IsaPlanner/rw_inst.ML Sat Mar 20 17:33:11 2010 +0100 @@ -297,7 +297,7 @@ |> Drule.implies_intr_list cprems |> Drule.forall_intr_list frees_of_fixed_vars |> Drule.forall_elim_list vars - |> Thm.varifyT' othertfrees + |> Thm.varifyT_global' othertfrees |-> K Drule.zero_var_indexes end; diff -r 65258d2c3214 -r e5980f0ad025 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Tools/nbe.ML Sat Mar 20 17:33:11 2010 +0100 @@ -102,12 +102,12 @@ o apfst (fst o fst o dest_TVar) o Logic.dest_of_class) prem_props; in Drule.implies_elim_list thm prem_thms end; in ct - |> Drule.cterm_rule Thm.varifyT + |> Drule.cterm_rule Thm.varifyT_global |> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) => (((v, 0), sort), TFree (v, sort'))) vs, [])) |> Drule.cterm_rule Thm.freezeT |> conv - |> Thm.varifyT + |> Thm.varifyT_global |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) => (((v, 0), []), TVar ((v, 0), sort))) vs, [])