--- a/src/HOL/Decision_Procs/approximation_generator.ML Fri Mar 06 23:14:41 2015 +0100
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Fri Mar 06 23:33:25 2015 +0100
@@ -117,7 +117,7 @@
}
fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)
-fun conv_term thy conv r = Thm.global_cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
+fun conv_term ctxt conv r = Thm.cterm_of ctxt r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
fun approx_random ctxt prec eps frees e xs genuine_only size seed =
let
@@ -138,7 +138,7 @@
(AList.lookup op = (map dest_Free xs ~~ ts)
#> the_default Term.dummy
#> curry op $ @{term "real::float\<Rightarrow>_"}
- #> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt postproc_form_eqs))
+ #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
frees
in
if approximate ctxt (mk_approx_form e ts) |> is_True
@@ -159,13 +159,12 @@
"\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
"\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
"\<not> \<not> q \<longleftrightarrow> q"
- by auto
- }
+ by auto}
fun reify_goal ctxt t =
HOLogic.mk_not t
- |> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt preproc_form_eqs)
- |> conv_term (Proof_Context.theory_of ctxt) (Reification.conv ctxt form_equations)
+ |> conv_term ctxt (rewrite_with ctxt preproc_form_eqs)
+ |> conv_term ctxt (Reification.conv ctxt form_equations)
|> dest_interpret_form
||> HOLogic.dest_list
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Mar 06 23:14:41 2015 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Mar 06 23:33:25 2015 +0100
@@ -76,12 +76,11 @@
fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) =
if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then
let
- val thy = Proof_Context.theory_of ctxt;
val fs = Misc_Legacy.term_frees eq;
- val cvs = Thm.global_cterm_of thy (HOLogic.mk_list T fs);
- val clhs = Thm.global_cterm_of thy (reif_polex T fs lhs);
- val crhs = Thm.global_cterm_of thy (reif_polex T fs rhs);
- val ca = Thm.global_ctyp_of thy T;
+ val cvs = Thm.cterm_of ctxt (HOLogic.mk_list T fs);
+ val clhs = Thm.cterm_of ctxt (reif_polex T fs lhs);
+ val crhs = Thm.cterm_of ctxt (reif_polex T fs rhs);
+ val ca = Thm.ctyp_of ctxt T;
in (ca, cvs, clhs, crhs) end
else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort)
| reif_eq _ _ = error "reif_eq: not an equation";
--- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 06 23:14:41 2015 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 06 23:33:25 2015 +0100
@@ -40,7 +40,6 @@
fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
let
- val thy = Proof_Context.theory_of ctxt;
(* Transform the term*)
val (t, np, nh) = prepare_for_linz q g;
(* Some simpsets for dealing with mod div abs and nat*)
@@ -73,7 +72,7 @@
|> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
(* simp rules for elimination of abs *)
val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
- val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
+ val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
[simp_tac mod_div_simpset 1, simp_tac simpset0 1,
@@ -86,7 +85,7 @@
(case Thm.prop_of pre_thm of
Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let
- val pth = linzqe_oracle (Thm.global_cterm_of thy (Envir.eta_long [] t1))
+ val pth = linzqe_oracle (Thm.cterm_of ctxt (Envir.eta_long [] t1))
in
((pth RS iffD2) RS pre_thm,
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 06 23:14:41 2015 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 06 23:33:25 2015 +0100
@@ -50,12 +50,11 @@
THEN' (REPEAT_DETERM o split_tac ctxt [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
THEN' SUBGOAL (fn (g, i) =>
let
- val thy = Proof_Context.theory_of ctxt
(* Transform the term*)
val (t,np,nh) = prepare_for_linr q g
(* Some simpsets for dealing with mod div abs and nat*)
val simpset0 = put_simpset HOL_basic_ss ctxt addsimps comp_arith
- val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
+ val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
[simp_tac simpset0 1,
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 06 23:14:41 2015 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 06 23:33:25 2015 +0100
@@ -70,7 +70,6 @@
THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
THEN' SUBGOAL (fn (g, i) =>
let
- val thy = Proof_Context.theory_of ctxt
(* Transform the term*)
val (t,np,nh) = prepare_for_mir q g
(* Some simpsets for dealing with mod div abs and nat*)
@@ -101,7 +100,7 @@
@{thm "int_0"}, @{thm "int_1"}]
|> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
(* simp rules for elimination of abs *)
- val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
+ val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
[simp_tac mod_div_simpset 1, simp_tac simpset0 1,
@@ -116,8 +115,8 @@
let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
if Config.get ctxt quick_and_dirty
- then mirfr_oracle (false, Thm.global_cterm_of thy (Envir.eta_long [] t1))
- else mirfr_oracle (true, Thm.global_cterm_of thy (Envir.eta_long [] t1))
+ then mirfr_oracle (false, Thm.cterm_of ctxt (Envir.eta_long [] t1))
+ else mirfr_oracle (true, Thm.cterm_of ctxt (Envir.eta_long [] t1))
in
((pth RS iffD2) RS pre_thm,
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))