--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Sun Feb 18 15:05:21 2018 +0100
@@ -737,7 +737,7 @@
(case get_matching_rules ctxt (Ring_Simps.get (Context.Proof ctxt)) t of
SOME (ths1, ths2, ths3, ths4, th5, th) =>
let val tr =
- Thm.transfer (Proof_Context.theory_of ctxt) #>
+ Thm.transfer' ctxt #>
(case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end
| NONE => error "get_ring_simps: lookup failed");
--- a/src/HOL/Decision_Procs/Reflective_Field.thy Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Sun Feb 18 15:05:21 2018 +0100
@@ -757,7 +757,7 @@
(case get_matching_rules ctxt (Field_Simps.get (Context.Proof ctxt)) t of
SOME (ths1, ths2, ths3, th4, th) =>
let val tr =
- Thm.transfer (Proof_Context.theory_of ctxt) #>
+ Thm.transfer' ctxt #>
(case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
in (map tr ths1, map tr ths2, map tr ths3, tr th4, tr th) end
| NONE => error "get_field_simps: lookup failed");
--- a/src/HOL/Library/conditional_parametricity.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Library/conditional_parametricity.ML Sun Feb 18 15:05:21 2018 +0100
@@ -457,7 +457,7 @@
Option.filter (is_parametricity_theorem andf (not o curry Term.could_unify
(Thm.full_prop_of @{thm is_equality_Rel})) o Thm.full_prop_of) o preprocess_theorem ctxt;
in
- map_filter (parametricity_thm_map_filter o Thm.transfer (Proof_Context.theory_of ctxt))
+ map_filter (parametricity_thm_map_filter o Thm.transfer' ctxt)
(Transfer.get_transfer_raw ctxt)
end;
--- a/src/HOL/Probability/Giry_Monad.thy Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Sun Feb 18 15:05:21 2018 +0100
@@ -194,7 +194,7 @@
fun subprob_cong thm ctxt = (
let
- val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm
+ val thm' = Thm.transfer' ctxt thm
val free = thm' |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
dest_comb |> snd |> strip_abs_body |> head_of |> is_Free
in
--- a/src/HOL/Tools/Function/function_context_tree.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Tools/Function/function_context_tree.ML Sun Feb 18 15:05:21 2018 +0100
@@ -53,7 +53,7 @@
fun get_function_congs ctxt =
FunctionCongs.get (Context.Proof ctxt)
- |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+ |> map (Thm.transfer' ctxt);
val add_function_cong = FunctionCongs.map o Thm.add_thm o Thm.trim_context;
--- a/src/HOL/Tools/inductive.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Feb 18 15:05:21 2018 +0100
@@ -276,7 +276,7 @@
fun get_monos ctxt =
#monos (rep_data ctxt)
- |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+ |> map (Thm.transfer' ctxt);
fun mk_mono ctxt thm =
let
@@ -314,7 +314,7 @@
fun retrieve_equations ctxt =
Item_Net.retrieve (#equations (rep_data ctxt))
- #> map (Thm.transfer (Proof_Context.theory_of ctxt));
+ #> map (Thm.transfer' ctxt);
val equation_add_permissive =
Thm.declaration_attribute (fn thm =>
--- a/src/HOL/Tools/lin_arith.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Feb 18 15:05:21 2018 +0100
@@ -87,7 +87,7 @@
fun get_splits ctxt =
#splits (get_arith_data ctxt)
- |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+ |> map (Thm.transfer' ctxt);
fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
{splits = update Thm.eq_thm_prop (Thm.trim_context thm) splits,
--- a/src/Provers/Arith/fast_lin_arith.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Sun Feb 18 15:05:21 2018 +0100
@@ -149,7 +149,7 @@
val map_data = Data.map;
val get_data = Data.get o Context.Proof;
-fun get_neqE ctxt = map (Thm.transfer (Proof_Context.theory_of ctxt)) (#neqE (get_data ctxt));
+fun get_neqE ctxt = map (Thm.transfer' ctxt) (#neqE (get_data ctxt));
fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
--- a/src/Provers/classical.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Provers/classical.ML Sun Feb 18 15:05:21 2018 +0100
@@ -196,7 +196,7 @@
trying rules in order. *)
fun swap_res_tac ctxt rls =
let
- val transfer = Thm.transfer (Proof_Context.theory_of ctxt);
+ val transfer = Thm.transfer' ctxt;
fun addrl rl brls = (false, transfer rl) :: (true, transfer rl RSN (2, Data.swap)) :: brls;
in
assume_tac ctxt ORELSE'
--- a/src/Provers/splitter.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Provers/splitter.ML Sun Feb 18 15:05:21 2018 +0100
@@ -440,7 +440,7 @@
val (name, asm) = split_thm_info split
val split0 = Thm.trim_context split
fun tac ctxt' =
- let val split' = Thm.transfer (Proof_Context.theory_of ctxt') split0 in
+ let val split' = Thm.transfer' ctxt' split0 in
(if asm then split_asm_tac ctxt' [split']
else if bang
then split_tac ctxt' [split'] THEN_ALL_NEW
--- a/src/Pure/Isar/code.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/Isar/code.ML Sun Feb 18 15:05:21 2018 +0100
@@ -1105,7 +1105,7 @@
singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt)
fun preprocess conv ctxt =
- Thm.transfer (Proof_Context.theory_of ctxt)
+ Thm.transfer' ctxt
#> rewrite_eqn conv ctxt
#> Axclass.unoverload ctxt;
--- a/src/Pure/Isar/context_rules.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/Isar/context_rules.ML Sun Feb 18 15:05:21 2018 +0100
@@ -161,7 +161,7 @@
fun find_rules_netpair ctxt weighted facts goal (inet, enet) =
find_erules weighted facts enet @ find_irules weighted goal inet
- |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+ |> map (Thm.transfer' ctxt);
fun find_rules ctxt weighted facts goal =
map (find_rules_netpair ctxt weighted facts goal) (netpairs ctxt);
--- a/src/Pure/Isar/locale.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/Isar/locale.ML Sun Feb 18 15:05:21 2018 +0100
@@ -648,8 +648,7 @@
);
fun get_thms which ctxt =
- map (Thm.transfer (Proof_Context.theory_of ctxt))
- (which (Thms.get (Context.Proof ctxt)));
+ map (Thm.transfer' ctxt) (which (Thms.get (Context.Proof ctxt)));
val get_witnesses = get_thms #1;
val get_intros = get_thms #2;
--- a/src/Pure/Isar/spec_rules.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/Isar/spec_rules.ML Sun Feb 18 15:05:21 2018 +0100
@@ -57,7 +57,7 @@
fun retrieve_generic context =
Item_Net.retrieve (Rules.get context)
- #> (map o apsnd o apsnd o map) (Thm.transfer (Context.theory_of context));
+ #> (map o apsnd o apsnd o map) (Thm.transfer'' context);
val retrieve = retrieve_generic o Context.Proof;
val retrieve_global = retrieve_generic o Context.Theory;
--- a/src/Pure/Isar/subgoal.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/Isar/subgoal.ML Sun Feb 18 15:05:21 2018 +0100
@@ -44,7 +44,7 @@
fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
let
val st = raw_st
- |> Thm.transfer (Proof_Context.theory_of ctxt)
+ |> Thm.transfer' ctxt
|> Raw_Simplifier.norm_hhf_protect ctxt;
val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1;
--- a/src/Pure/Proof/proof_syntax.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Sun Feb 18 15:05:21 2018 +0100
@@ -244,7 +244,7 @@
fun proof_of ctxt full raw_thm =
let
- val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm;
+ val thm = Thm.transfer' ctxt raw_thm;
val prop = Thm.full_prop_of thm;
val prf = Thm.proof_of thm;
val prf' =
--- a/src/Pure/Proof/reconstruct.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/Proof/reconstruct.ML Sun Feb 18 15:05:21 2018 +0100
@@ -332,7 +332,7 @@
val prop_of = prop_of' [];
fun proof_of ctxt raw_thm =
- let val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm
+ let val thm = Thm.transfer' ctxt raw_thm
in reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
--- a/src/Pure/Tools/named_theorems.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/Tools/named_theorems.ML Sun Feb 18 15:05:21 2018 +0100
@@ -52,7 +52,7 @@
fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt);
fun content context =
- rev o map (Thm.transfer (Context.theory_of context)) o Item_Net.content o the_entry context;
+ rev o map (Thm.transfer'' context) o Item_Net.content o the_entry context;
val get = content o Context.Proof;
--- a/src/Pure/facts.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/facts.ML Sun Feb 18 15:05:21 2018 +0100
@@ -195,7 +195,7 @@
in
{name = name,
dynamic = dynamic,
- thms = map (Thm.transfer (Context.theory_of context)) thms}
+ thms = map (Thm.transfer'' context) thms}
end;
--- a/src/Pure/more_thm.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/more_thm.ML Sun Feb 18 15:05:21 2018 +0100
@@ -617,7 +617,7 @@
let val (x', th') = f (x, th) in (SOME x', SOME th') end;
fun apply_attribute (att: attribute) th x =
- let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
+ let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th))
in (the_default th th', the_default x x') end;
fun attribute_declaration att th x = #2 (apply_attribute att th x);
@@ -685,7 +685,7 @@
val show_hyps = Config.get ctxt show_hyps;
val th = raw_th
- |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt)))
+ |> perhaps (try (Thm.transfer' ctxt))
|> perhaps (try Thm.strip_shyps);
val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th;
--- a/src/Pure/raw_simplifier.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/raw_simplifier.ML Sun Feb 18 15:05:21 2018 +0100
@@ -579,8 +579,7 @@
local
fun comb_simps ctxt comb mk_rrule thms =
- let
- val rews = extract_rews ctxt (map (Thm.transfer (Proof_Context.theory_of ctxt)) thms);
+ let val rews = extract_rews ctxt (map (Thm.transfer' ctxt) thms);
in fold (fold comb o mk_rrule) rews ctxt end;
in
@@ -1388,7 +1387,7 @@
local
fun gen_norm_hhf ss ctxt =
- Thm.transfer (Proof_Context.theory_of ctxt) #>
+ Thm.transfer' ctxt #>
(fn th =>
if Drule.is_norm_hhf (Thm.prop_of th) then th
else
--- a/src/Pure/thm.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/thm.ML Sun Feb 18 15:05:21 2018 +0100
@@ -79,6 +79,8 @@
val trim_context: thm -> thm
val transfer_cterm: theory -> cterm -> cterm
val transfer: theory -> thm -> thm
+ val transfer': Proof.context -> thm -> thm
+ val transfer'': Context.generic -> thm -> thm
val renamed_prop: term -> thm -> thm
val weaken: cterm -> thm -> thm
val weaken_sorts: sort list -> cterm -> cterm
@@ -457,6 +459,9 @@
prop = prop})
end;
+val transfer' = transfer o Proof_Context.theory_of;
+val transfer'' = transfer o Context.theory_of;
+
(* matching *)
--- a/src/Tools/Code/code_runtime.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Tools/Code/code_runtime.ML Sun Feb 18 15:05:21 2018 +0100
@@ -354,7 +354,7 @@
fun get ctxt =
Computation_Preproc_Data.get (Proof_Context.theory_of ctxt)
- |> map (Thm.transfer (Proof_Context.theory_of ctxt))
+ |> map (Thm.transfer' ctxt)
in
--- a/src/Tools/induct.ML Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Tools/induct.ML Sun Feb 18 15:05:21 2018 +0100
@@ -277,11 +277,11 @@
fun lookup_rule which ctxt =
AList.lookup (op =) (Item_Net.content (which (get_local ctxt)))
- #> Option.map (Thm.transfer (Proof_Context.theory_of ctxt));
+ #> Option.map (Thm.transfer' ctxt);
fun find_rules which how ctxt x =
Item_Net.retrieve (which (get_local ctxt)) (how x)
- |> map (Thm.transfer (Proof_Context.theory_of ctxt) o snd);
+ |> map (Thm.transfer' ctxt o snd);
in