--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 06 23:56:43 2015 +0100
@@ -469,7 +469,7 @@
val T = mk_tupleT_balanced tfrees;
in
@{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
- |> Drule.instantiate' [SOME (Thm.global_ctyp_of @{theory} T)] []
+ |> Drule.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
|> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
|> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
|> Thm.varifyT_global
--- a/src/HOL/Tools/Transfer/transfer.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML Fri Mar 06 23:56:43 2015 +0100
@@ -222,7 +222,6 @@
fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
let
- val thy = Thm.theory_of_thm thm
val prop = Thm.prop_of thm
val (t, mk_prop') = dest prop
(* Only consider "op =" at non-base types *)
@@ -238,7 +237,7 @@
val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
- val cprop = Thm.global_cterm_of thy prop2
+ val cprop = Thm.cterm_of ctxt prop2
val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
in
@@ -317,7 +316,6 @@
fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
let
- val thy = Thm.theory_of_thm thm
val prop = Thm.prop_of thm
val (t, mk_prop') = dest prop
val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
@@ -331,7 +329,7 @@
val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
val prop2 = Logic.list_rename_params (rev names) prop1
- val cprop = Thm.global_cterm_of thy prop2
+ val cprop = Thm.cterm_of ctxt prop2
val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
in
@@ -415,60 +413,59 @@
fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
let
- val thy = Proof_Context.theory_of ctxt
(* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
- let
- val r1 = rel T1 U1
- val r2 = rel T2 U2
- val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
- in
- Const (@{const_name rel_fun}, rT) $ r1 $ r2
- end
+ let
+ val r1 = rel T1 U1
+ val r2 = rel T2 U2
+ val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
+ in
+ Const (@{const_name rel_fun}, rT) $ r1 $ r2
+ end
| rel T U =
- let
- val (a, _) = dest_TFree (prj (T, U))
- in
- Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
- end
+ let
+ val (a, _) = dest_TFree (prj (T, U))
+ in
+ Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
+ end
fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
| zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
- let
- val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
- val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
- val cprop = Thm.global_cterm_of thy (HOLogic.mk_Trueprop prop)
- val thm0 = Thm.assume cprop
- val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
- val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
- val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1))
- val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r1))
- val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
- val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
- val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
- val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
- val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
- in
- (thm2 COMP rule, hyps)
- end
+ let
+ val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
+ val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
+ val cprop = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop prop)
+ val thm0 = Thm.assume cprop
+ val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
+ val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
+ val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1))
+ val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r1))
+ val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
+ val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
+ val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
+ val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
+ val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
+ in
+ (thm2 COMP rule, hyps)
+ end
| zip ctxt thms (f $ t) (g $ u) =
- let
- val (thm1, hyps1) = zip ctxt thms f g
- val (thm2, hyps2) = zip ctxt thms t u
- in
- (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
- end
+ let
+ val (thm1, hyps1) = zip ctxt thms f g
+ val (thm2, hyps2) = zip ctxt thms t u
+ in
+ (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
+ end
| zip _ _ t u =
- let
- val T = fastype_of t
- val U = fastype_of u
- val prop = mk_Rel (rel T U) $ t $ u
- val cprop = Thm.global_cterm_of thy (HOLogic.mk_Trueprop prop)
- in
- (Thm.assume cprop, [cprop])
- end
+ let
+ val T = fastype_of t
+ val U = fastype_of u
+ val prop = mk_Rel (rel T U) $ t $ u
+ val cprop = Thm.cterm_of ctxt (HOLogic.mk_Trueprop prop)
+ in
+ (Thm.assume cprop, [cprop])
+ end
val r = mk_Rel (rel (fastype_of t) (fastype_of u))
val goal = HOLogic.mk_Trueprop (r $ t $ u)
- val rename = Thm.trivial (Thm.global_cterm_of thy goal)
+ val rename = Thm.trivial (Thm.cterm_of ctxt goal)
val (thm, hyps) = zip ctxt [] t u
in
Drule.implies_intr_list hyps (thm RS rename)
@@ -577,10 +574,8 @@
val cbool = @{ctyp bool}
val relT = @{typ "bool => bool => bool"}
val idx = Thm.maxidx_of thm + 1
- val thy = Proof_Context.theory_of ctxt
- fun tinst (a, _) = (Thm.global_ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
- fun inst (a, t) =
- (Thm.global_cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), Thm.global_cterm_of thy t)
+ fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
+ fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
in
thm
|> Thm.generalize (tfrees, rnames @ frees) idx
@@ -603,10 +598,8 @@
val cbool = @{ctyp bool}
val relT = @{typ "bool => bool => bool"}
val idx = Thm.maxidx_of thm + 1
- val thy = Proof_Context.theory_of ctxt
- fun tinst (a, _) = (Thm.global_ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
- fun inst (a, t) =
- (Thm.global_cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), Thm.global_cterm_of thy t)
+ fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
+ fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
in
thm
|> Thm.generalize (tfrees, rnames @ frees) idx
--- a/src/HOL/Tools/choice_specification.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/choice_specification.ML Fri Mar 06 23:56:43 2015 +0100
@@ -83,7 +83,7 @@
val ctxt = Proof_Context.init_global thy
val rew_imps = alt_props |>
- map (Object_Logic.atomize ctxt o Thm.global_cterm_of thy o Syntax.read_prop_global thy o snd)
+ map (Object_Logic.atomize ctxt o Thm.cterm_of ctxt o Syntax.read_prop_global thy o snd)
val props' = rew_imps |>
map (HOLogic.dest_Trueprop o Thm.term_of o snd o Thm.dest_equals o Thm.cprop_of)
--- a/src/HOL/Tools/cnf.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/cnf.ML Fri Mar 06 23:56:43 2015 +0100
@@ -259,14 +259,13 @@
fun make_under_quantifiers ctxt make t =
let
- val thy = Proof_Context.theory_of ctxt
fun conv ctxt ct =
(case Thm.term_of ct of
Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
| Abs _ => Conv.abs_conv (conv o snd) ctxt ct
| Const _ => Conv.all_conv ct
| t => make t RS eq_reflection)
- in conv ctxt (Thm.global_cterm_of thy t) RS meta_eq_to_obj_eq end
+ in conv ctxt (Thm.cterm_of ctxt t) RS meta_eq_to_obj_eq end
fun make_nnf_thm_under_quantifiers ctxt =
make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
--- a/src/HOL/Tools/datatype_realizer.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Mar 06 23:56:43 2015 +0100
@@ -105,11 +105,11 @@
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
- val inst = map (apply2 (Thm.global_cterm_of thy)) (map head_of (HOLogic.dest_conj
+ val inst = map (apply2 (Thm.cterm_of ctxt)) (map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
val thm =
- Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems) (Thm.global_cterm_of thy concl)
+ Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
(fn prems =>
EVERY [
rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
@@ -185,12 +185,12 @@
val y' = Free ("y", T);
val thm =
- Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems)
- (Thm.global_cterm_of thy
+ Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems)
+ (Thm.cterm_of ctxt
(HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
(fn prems =>
EVERY [
- rtac (cterm_instantiate [apply2 (Thm.global_cterm_of thy) (y, y')] exhaust) 1,
+ rtac (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust) 1,
ALLGOALS (EVERY'
[asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
--- a/src/HOL/Tools/inductive.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Mar 06 23:56:43 2015 +0100
@@ -565,15 +565,13 @@
fun mk_cases ctxt prop =
let
- val thy = Proof_Context.theory_of ctxt;
-
fun err msg =
error (Pretty.string_of (Pretty.block
[Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
val elims = Induct.find_casesP ctxt prop;
- val cprop = Thm.global_cterm_of thy prop;
+ val cprop = Thm.cterm_of ctxt prop;
fun mk_elim rl =
Thm.implies_intr cprop
(Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
@@ -636,7 +634,7 @@
| _ => error
("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique"));
val inst =
- map (fn v => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy (Envir.subst_term subst (Var v))))
+ map (fn v => apply2 (Thm.cterm_of ctxt') (Var v, Envir.subst_term subst (Var v)))
(Term.add_vars (lhs_of eq) []);
in
Drule.cterm_instantiate inst eq
--- a/src/HOL/Tools/inductive_set.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/inductive_set.ML Fri Mar 06 23:56:43 2015 +0100
@@ -41,10 +41,9 @@
fun strong_ind_simproc tab =
Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn ctxt => fn t =>
let
- val thy = Proof_Context.theory_of ctxt;
fun close p t f =
let val vs = Term.add_vars t []
- in Drule.instantiate' [] (rev (map (SOME o Thm.global_cterm_of thy o Var) vs))
+ in Drule.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
(p (fold (Logic.all o Var) vs t) f)
end;
fun mkop @{const_name HOL.conj} T x =
@@ -93,8 +92,8 @@
in
if forall is_none rews then NONE
else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1)
- (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.global_cterm_of thy)
- rews ts) (Thm.reflexive (Thm.global_cterm_of thy h)))
+ (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.cterm_of ctxt)
+ rews ts) (Thm.reflexive (Thm.cterm_of ctxt h)))
end
| NONE => NONE)
| _ => NONE
@@ -200,7 +199,7 @@
(* 3. simplify *)
(**************************************************************)
-fun mk_to_pred_inst thy fs =
+fun mk_to_pred_inst ctxt fs =
map (fn (x, ps) =>
let
val (Ts, T) = strip_type (fastype_of x);
@@ -208,8 +207,8 @@
val x' = map_type
(K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
in
- (Thm.global_cterm_of thy x,
- Thm.global_cterm_of thy (fold_rev (Term.abs o pair "x") Ts
+ (Thm.cterm_of ctxt x,
+ Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
(HOLogic.Collect_const U $
HOLogic.mk_psplits ps U HOLogic.boolT
(list_comb (x', map Bound (length Ts - 1 downto 0))))))
@@ -217,8 +216,7 @@
fun mk_to_pred_eq ctxt p fs optfs' T thm =
let
- val thy = Thm.theory_of_thm thm;
- val insts = mk_to_pred_inst thy fs;
+ val insts = mk_to_pred_inst ctxt fs;
val thm' = Thm.instantiate ([], insts) thm;
val thm'' =
(case optfs' of
@@ -233,7 +231,7 @@
Thm.dest_comb |> snd |> Drule.strip_comb |> snd |> hd |> Thm.dest_comb
in
thm' RS (Drule.cterm_instantiate [(arg_cong_f,
- Thm.global_cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
+ Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
end)
@@ -322,7 +320,8 @@
lookup_rule (Proof_Context.theory_of ctxt) (Thm.prop_of #> Logic.dest_equals) rules')
end;
-fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
+fun to_pred_proc thy rules t =
+ case lookup_rule thy I rules t of
NONE => NONE
| SOME (lhs, rhs) =>
SOME (Envir.subst_term
@@ -337,7 +336,7 @@
val fs = filter (is_Var o fst)
(infer_arities thy set_arities (NONE, Thm.prop_of thm) []);
(* instantiate each set parameter with {(x, y). p x y} *)
- val insts = mk_to_pred_inst thy fs
+ val insts = mk_to_pred_inst ctxt fs
in
thm |>
Thm.instantiate ([], insts) |>
@@ -370,8 +369,8 @@
val T = HOLogic.mk_ptupleT ps Us;
val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x
in
- (Thm.global_cterm_of thy x,
- Thm.global_cterm_of thy (fold_rev (Term.abs o pair "x") Ts
+ (Thm.cterm_of ctxt x,
+ Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
(HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)),
list_comb (x', map Bound (l - 1 downto k + 1))))))
end) fs;
--- a/src/HOL/Tools/monomorph.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/monomorph.ML Fri Mar 06 23:56:43 2015 +0100
@@ -157,9 +157,9 @@
(* collecting instances *)
-fun instantiate thy subst =
+fun instantiate ctxt subst =
let
- fun cert (ix, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar (ix, S), T)
+ fun cert (ix, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (ix, S), T)
fun cert' subst = Vartab.fold (cons o cert) subst []
in Thm.instantiate (cert' subst, []) end
@@ -186,7 +186,7 @@
raise ENOUGH cx
else
let
- val thm' = instantiate thy subst thm
+ val thm' = instantiate ctxt subst thm
val rthm = ((round, subst), thm')
val rthms = Inttab.lookup_list insts id;
val n_insts' =
--- a/src/HOL/Tools/numeral.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/numeral.ML Fri Mar 06 23:56:43 2015 +0100
@@ -44,10 +44,10 @@
val oneT = Thm.ctyp_of_cterm one;
val numeral = @{cpat "numeral"};
-val numeralT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral));
+val numeralT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm numeral));
val uminus = @{cpat "uminus"};
-val uminusT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus));
+val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus));
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
--- a/src/HOL/Tools/numeral_simprocs.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Fri Mar 06 23:56:43 2015 +0100
@@ -483,7 +483,7 @@
simplify_one ctxt (([th, cancel_th]) MRS trans);
local
- val Tp_Eq = Thm.reflexive (Thm.global_cterm_of @{theory HOL} HOLogic.Trueprop)
+ val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop)
fun Eq_True_elim Eq =
Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
in
@@ -492,9 +492,8 @@
val zero = Const(@{const_name Groups.zero}, T);
val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
val pos = less $ zero $ t and neg = less $ t $ zero
- val thy = Proof_Context.theory_of ctxt
fun prove p =
- SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.global_cterm_of thy p)))
+ SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.cterm_of ctxt p)))
handle THM _ => NONE
in case prove pos of
SOME th => SOME(th RS pos_th)
--- a/src/HOL/Tools/record.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/record.ML Fri Mar 06 23:56:43 2015 +0100
@@ -1375,9 +1375,9 @@
fun mk_split_free_tac free induct_thm i =
let
- val cfree = Thm.global_cterm_of thy free;
+ val cfree = Thm.cterm_of ctxt free;
val _$ (_ $ r) = Thm.concl_of induct_thm;
- val crec = Thm.global_cterm_of thy r;
+ val crec = Thm.cterm_of ctxt r;
val thm = cterm_instantiate [(crec, cfree)] induct_thm;
in
simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) i THEN
@@ -1606,7 +1606,7 @@
(roughly) the definition of the accessor.*)
val surject = timeit_msg ctxt "record extension surjective proof:" (fn () =>
let
- val cterm_ext = Thm.global_cterm_of defs_thy ext;
+ val cterm_ext = Thm.cterm_of defs_ctxt ext;
val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
val tactic1 =
simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
@@ -1943,8 +1943,8 @@
fun to_Var (Free (c, T)) = Var ((c, 1), T);
in mk_rec (map to_Var all_vars_more) 0 end;
- val cterm_rec = Thm.global_cterm_of ext_thy r_rec0;
- val cterm_vrs = Thm.global_cterm_of ext_thy r_rec0_Vars;
+ val cterm_rec = Thm.cterm_of ext_ctxt r_rec0;
+ val cterm_vrs = Thm.cterm_of ext_ctxt r_rec0_Vars;
val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
val init_thm = named_cterm_instantiate insts updacc_eq_triv;
val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
--- a/src/HOL/Tools/reification.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/reification.ML Fri Mar 06 23:56:43 2015 +0100
@@ -169,12 +169,12 @@
val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv);
val (fts, its) =
(map (snd o snd) fnvs,
- map (fn ((vn, vi), (tT, t)) => apply2 (Thm.global_cterm_of thy) (Var ((vn, vi), tT), t)) invs);
+ map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt) (Var ((vn, vi), tT), t)) invs);
val ctyenv =
- map (fn ((vn, vi), (s, ty)) => apply2 (Thm.global_ctyp_of thy) (TVar ((vn, vi), s), ty))
+ map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar ((vn, vi), s), ty))
(Vartab.dest tyenv);
in
- ((map (Thm.global_cterm_of thy) fts ~~ replicate (length fts) ctxt,
+ ((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt,
apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds))
end;
@@ -203,14 +203,14 @@
val sbst = Envir.subst_term (tyenv, tmenv);
val sbsT = Envir.subst_type tyenv;
val subst_ty =
- map (fn (n, (s, t)) => apply2 (Thm.global_ctyp_of thy) (TVar (n, s), t)) (Vartab.dest tyenv)
+ map (fn (n, (s, t)) => apply2 (Thm.ctyp_of ctxt'') (TVar (n, s), t)) (Vartab.dest tyenv)
val tml = Vartab.dest tmenv;
val (subst_ns, bds) = fold_map
(fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
let
val name = snd (the (AList.lookup (op =) tml xn0));
val (idx, bds) = index_of name bds;
- in (apply2 (Thm.global_cterm_of thy) (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
+ in (apply2 (Thm.cterm_of ctxt'') (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
val subst_vs =
let
fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) =
@@ -220,10 +220,10 @@
val (bsT, _) = the (AList.lookup Type.could_unify bds lT);
val vsn = the (AList.lookup (op =) vsns_map vs);
val vs' = fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT'));
- in apply2 (Thm.global_cterm_of thy) (vs, vs') end;
+ in apply2 (Thm.cterm_of ctxt'') (vs, vs') end;
in map h subst end;
val cts =
- map (fn ((vn, vi), (tT, t)) => apply2 (Thm.global_cterm_of thy) (Var ((vn, vi), tT), t))
+ map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt'') (Var ((vn, vi), tT), t))
(fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
(map (fn n => (n, 0)) xns) tml);
val substt =
--- a/src/HOL/Tools/sat.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/sat.ML Fri Mar 06 23:56:43 2015 +0100
@@ -73,7 +73,7 @@
val resolution_thm =
@{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
-val cP = Thm.global_cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
+val cP = Thm.cterm_of @{context} (Var (("P", 0), HOLogic.boolT));
(* ------------------------------------------------------------------------- *)
(* lit_ord: an order on integers that considers their absolute values only, *)
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Mar 06 23:56:43 2015 +0100
@@ -903,9 +903,8 @@
fun prover ctxt thms Tconcl (js : injust list) split_neq pos : thm option =
let
- val thy = Proof_Context.theory_of ctxt
val nTconcl = LA_Logic.neg_prop Tconcl
- val cnTconcl = Thm.global_cterm_of thy nTconcl
+ val cnTconcl = Thm.cterm_of ctxt nTconcl
val nTconclthm = Thm.assume cnTconcl
val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm])
val (Falsethm, _) = fwdproof ctxt tree js
--- a/src/Provers/hypsubst.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Provers/hypsubst.ML Fri Mar 06 23:56:43 2015 +0100
@@ -168,7 +168,6 @@
Data.dest_Trueprop #> Data.dest_eq #> apply2 contract) (Thm.term_of cBi) of
SOME (t, t') =>
let
- val thy = Proof_Context.theory_of ctxt;
val Bi = Thm.term_of cBi;
val ps = Logic.strip_params Bi;
val U = Term.fastype_of1 (rev (map snd ps), t);
@@ -184,10 +183,10 @@
(case (if b then t else t') of
Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
| t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
- val (instT, _) = Thm.match (apply2 (Thm.global_cterm_of thy o Logic.mk_type) (V, U));
+ val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U));
in
compose_tac ctxt (true, Drule.instantiate_normalize (instT,
- map (apply2 (Thm.global_cterm_of thy))
+ map (apply2 (Thm.cterm_of ctxt))
[(Var (ixn, Ts ---> U --> body_type T), u),
(Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
(Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
--- a/src/Tools/coherent.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Tools/coherent.ML Fri Mar 06 23:56:43 2015 +0100
@@ -173,19 +173,16 @@
fun thm_of_cl_prf ctxt goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
let
- val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.global_cterm_of thy;
- val certT = Thm.global_ctyp_of thy;
val _ =
cond_trace ctxt (fn () =>
Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms)));
val th' =
Drule.implies_elim_list
(Thm.instantiate
- (map (fn (ixn, (S, T)) => (certT (TVar ((ixn, S))), certT T)) (Vartab.dest tye),
+ (map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) (Vartab.dest tye),
map (fn (ixn, (T, t)) =>
- (cert (Var (ixn, Envir.subst_type tye T)), cert t)) (Vartab.dest env) @
- map (fn (ixnT, t) => (cert (Var ixnT), cert t)) insts) th)
+ apply2 (Thm.cterm_of ctxt) (Var (ixn, Envir.subst_type tye T), t)) (Vartab.dest env) @
+ map (fn (ixnT, t) => apply2 (Thm.cterm_of ctxt) (Var ixnT, t)) insts) th)
(map (nth asms) is);
val (_, cases) = dest_elim (Thm.prop_of th');
in
@@ -201,10 +198,8 @@
and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) =
let
- val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.global_cterm_of thy;
- val cparams = map cert params;
- val asms'' = map (cert o curry subst_bounds (rev params)) asms';
+ val cparams = map (Thm.cterm_of ctxt) params;
+ val asms'' = map (Thm.cterm_of ctxt o curry subst_bounds (rev params)) asms';
val (prems'', ctxt') = fold_map Thm.assume_hyps asms'' ctxt;
in
Drule.forall_intr_list cparams
--- a/src/Tools/cong_tac.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Tools/cong_tac.ML Fri Mar 06 23:56:43 2015 +0100
@@ -14,7 +14,6 @@
fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
let
- val cert = Thm.global_cterm_of (Thm.theory_of_cterm cgoal);
val goal = Thm.term_of cgoal;
in
(case Logic.strip_assums_concl goal of
@@ -25,7 +24,7 @@
val ps = Logic.strip_params (Thm.concl_of cong');
val insts =
[(f', f), (g', g), (x', x), (y', y)]
- |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
+ |> map (fn (t, u) => apply2 (Thm.cterm_of ctxt) (Term.head_of t, fold_rev Term.abs ps u));
in
fn st =>
compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
--- a/src/Tools/eqsubst.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Tools/eqsubst.ML Fri Mar 06 23:56:43 2015 +0100
@@ -259,14 +259,11 @@
val th = Thm.incr_indexes 1 gth;
val tgt_term = Thm.prop_of th;
- val thy = Thm.theory_of_thm th;
- val cert = Thm.global_cterm_of thy;
-
val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
- val cfvs = rev (map cert fvs);
+ val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
val conclterm = Logic.strip_imp_concl fixedbody;
- val conclthm = Thm.trivial (cert conclterm);
+ val conclthm = Thm.trivial (Thm.cterm_of ctxt conclterm);
val maxidx = Thm.maxidx_of th;
val ft =
(Zipper.move_down_right (* ==> *)
@@ -274,7 +271,7 @@
o Zipper.mktop
o Thm.prop_of) conclthm
in
- ((cfvs, conclthm), (thy, maxidx, ft))
+ ((cfvs, conclthm), (Proof_Context.theory_of ctxt, maxidx, ft))
end;
(* substitute using an object or meta level equality *)
--- a/src/Tools/nbe.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Tools/nbe.ML Fri Mar 06 23:56:43 2015 +0100
@@ -580,10 +580,9 @@
fun mk_equals ctxt lhs raw_rhs =
let
- val thy = Proof_Context.theory_of ctxt;
val ty = Thm.typ_of_cterm lhs;
- val eq = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
- val rhs = Thm.global_cterm_of thy raw_rhs;
+ val eq = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
+ val rhs = Thm.cterm_of ctxt raw_rhs;
in Thm.mk_binop eq lhs rhs end;
val (_, raw_oracle) = Context.>>> (Context.map_theory_result