--- a/src/HOL/HOLCF/Tools/cont_proc.ML Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Fri Mar 06 23:57:01 2015 +0100
@@ -121,8 +121,7 @@
local
fun solve_cont ctxt t =
let
- val thy = Proof_Context.theory_of ctxt
- val tr = instantiate' [] [SOME (Thm.global_cterm_of thy t)] @{thm Eq_TrueI}
+ val tr = instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
in
fun cont_proc thy =
--- a/src/HOL/Library/Code_Abstract_Nat.thy Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Fri Mar 06 23:57:01 2015 +0100
@@ -56,10 +56,9 @@
fun remove_suc ctxt thms =
let
- val thy = Proof_Context.theory_of ctxt;
val vname = singleton (Name.variant_list (map fst
(fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
- val cv = Thm.global_cterm_of thy (Var ((vname, 0), HOLogic.natT));
+ val cv = Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT));
val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of;
val rhs_of = snd o Thm.dest_comb o Thm.cprop_of;
fun find_vars ct = (case Thm.term_of ct of
--- a/src/HOL/Library/Countable.thy Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Library/Countable.thy Fri Mar 06 23:57:01 2015 +0100
@@ -180,8 +180,7 @@
val alist = pred_names ~~ induct_thms
val induct_thm = the (AList.lookup (op =) alist pred_name)
val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
- val thy = Proof_Context.theory_of ctxt
- val insts = vars |> map (fn (_, T) => try (Thm.global_cterm_of thy)
+ val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
(Const (@{const_name Countable.finite_item}, T)))
val induct_thm' = Drule.instantiate' [] insts induct_thm
val rules = @{thms finite_item.intros}
--- a/src/HOL/NSA/transfer.ML Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/NSA/transfer.ML Fri Mar 06 23:57:01 2015 +0100
@@ -52,12 +52,11 @@
fun transfer_thm_of ctxt ths t =
let
- val thy = Proof_Context.theory_of ctxt;
val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
val meta = Local_Defs.meta_rewrite_rule ctxt;
val ths' = map meta ths;
val unfolds' = map meta unfolds and refolds' = map meta refolds;
- val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.global_cterm_of thy t))
+ val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t))
val u = unstar_term consts t'
val tac =
rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Fri Mar 06 23:57:01 2015 +0100
@@ -433,11 +433,11 @@
val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct1));
-val ct1' = Thm.global_cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
+val ct1' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
-val ct2' = Thm.global_cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
+val ct2' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
*}
end
--- a/src/HOL/Statespace/state_fun.ML Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Statespace/state_fun.ML Fri Mar 06 23:57:01 2015 +0100
@@ -53,26 +53,24 @@
val lazy_conj_simproc =
Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
(fn ctxt => fn t =>
- let val thy = Proof_Context.theory_of ctxt in
- (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) =>
- let
- val P_P' = Simplifier.rewrite ctxt (Thm.global_cterm_of thy P);
- val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2;
- in
- if isFalse P' then SOME (conj1_False OF [P_P'])
- else
- let
- val Q_Q' = Simplifier.rewrite ctxt (Thm.global_cterm_of thy Q);
- val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2;
- in
- if isFalse Q' then SOME (conj2_False OF [Q_Q'])
- else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
- else if P aconv P' andalso Q aconv Q' then NONE
- else SOME (conj_cong OF [P_P', Q_Q'])
- end
- end
- | _ => NONE)
- end);
+ (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) =>
+ let
+ val P_P' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt P);
+ val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2;
+ in
+ if isFalse P' then SOME (conj1_False OF [P_P'])
+ else
+ let
+ val Q_Q' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt Q);
+ val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2;
+ in
+ if isFalse Q' then SOME (conj2_False OF [Q_Q'])
+ else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
+ else if P aconv P' andalso Q aconv Q' then NONE
+ else SOME (conj_cong OF [P_P', Q_Q'])
+ end
+ end
+ | _ => NONE));
fun string_eq_simp_tac ctxt =
simp_tac (put_simpset HOL_basic_ss ctxt
@@ -113,7 +111,6 @@
(case t of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $
(s as Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _)) =>
(let
- val thy = Proof_Context.theory_of ctxt;
val (_::_::_::_::sT::_) = binder_types uT;
val mi = maxidx_of_term t;
fun mk_upds (Const (@{const_name StateFun.update}, uT) $ d' $ c $ m $ v $ s) =
@@ -141,7 +138,8 @@
| mk_upds s = (Var (("s", mi + 1), sT), mi + 2);
val ct =
- Thm.global_cterm_of thy (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ fst (mk_upds s));
+ Thm.cterm_of ctxt
+ (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ fst (mk_upds s));
val basic_ss = #1 (Data.get (Context.Proof ctxt));
val ctxt' = ctxt |> Config.put simp_depth_limit 100 |> put_simpset basic_ss;
val thm = Simplifier.rewrite ctxt' ct;
--- a/src/HOL/Word/WordBitwise.thy Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Word/WordBitwise.thy Fri Mar 06 23:57:01 2015 +0100
@@ -550,7 +550,6 @@
fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
let
- val thy = Proof_Context.theory_of ctxt;
val (f $ arg) = Thm.term_of ct;
val n = (case arg of @{term nat} $ n => n | n => n)
|> HOLogic.dest_number |> snd;
@@ -560,7 +559,7 @@
(replicate i @{term Suc});
val _ = if arg = arg' then raise TERM ("", []) else ();
fun propfn g = HOLogic.mk_eq (g arg, g arg')
- |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy;
+ |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
val eq1 = Goal.prove_internal ctxt [] (propfn I)
(K (simp_tac (put_simpset word_ss ctxt) 1));
in Goal.prove_internal ctxt [] (propfn (curry (op $) f))
--- a/src/HOL/ex/SAT_Examples.thy Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Fri Mar 06 23:57:01 2015 +0100
@@ -534,7 +534,7 @@
| and_to_list fm acc = rev (fm :: acc)
val clauses = and_to_list prop_fm []
val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
- val cterms = map (Thm.global_cterm_of @{theory}) terms
+ val cterms = map (Thm.cterm_of @{context}) terms
val start = Timing.start ()
val _ = SAT.rawsat_thm @{context} cterms
in
--- a/src/HOL/ex/SVC_Oracle.thy Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Mar 06 23:57:01 2015 +0100
@@ -111,9 +111,8 @@
fun svc_tac ctxt = CSUBGOAL (fn (ct, i) =>
let
- val thy = Thm.theory_of_cterm ct;
val (abs_goal, _) = svc_abstract (Thm.term_of ct);
- val th = svc_oracle (Thm.global_cterm_of thy abs_goal);
+ val th = svc_oracle (Thm.cterm_of ctxt abs_goal);
in compose_tac ctxt (false, th, 0) i end
handle TERM _ => no_tac);
*}