# HG changeset patch
# User wenzelm
# Date 1518962721 -3600
# Node ID 1e1782c1aedfd9e2f267a4fdb89c4106d0c73a54
# Parent  f6e351043014fe02f2df3ce3ec50578aada05f2c
tuned signature;

diff -r f6e351043014 -r 1e1782c1aedf src/HOL/Decision_Procs/Commutative_Ring.thy
--- 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");
diff -r f6e351043014 -r 1e1782c1aedf src/HOL/Decision_Procs/Reflective_Field.thy
--- 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");
diff -r f6e351043014 -r 1e1782c1aedf src/HOL/Library/conditional_parametricity.ML
--- 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;
 
diff -r f6e351043014 -r 1e1782c1aedf src/HOL/Probability/Giry_Monad.thy
--- 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
diff -r f6e351043014 -r 1e1782c1aedf src/HOL/Tools/Function/function_context_tree.ML
--- 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;
 
diff -r f6e351043014 -r 1e1782c1aedf src/HOL/Tools/inductive.ML
--- 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 =>
diff -r f6e351043014 -r 1e1782c1aedf src/HOL/Tools/lin_arith.ML
--- 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,
diff -r f6e351043014 -r 1e1782c1aedf src/Provers/Arith/fast_lin_arith.ML
--- 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,
diff -r f6e351043014 -r 1e1782c1aedf src/Provers/classical.ML
--- 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'
diff -r f6e351043014 -r 1e1782c1aedf src/Provers/splitter.ML
--- 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
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/Isar/code.ML
--- 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;
 
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/Isar/context_rules.ML
--- 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);
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/Isar/locale.ML
--- 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;
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/Isar/spec_rules.ML
--- 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;
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/Isar/subgoal.ML
--- 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;
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/Proof/proof_syntax.ML
--- 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' =
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/Proof/reconstruct.ML
--- 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;
 
 
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/Tools/named_theorems.ML
--- 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;
 
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/facts.ML
--- 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;
 
 
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/more_thm.ML
--- 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;
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/raw_simplifier.ML
--- 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
diff -r f6e351043014 -r 1e1782c1aedf src/Pure/thm.ML
--- 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 *)
 
diff -r f6e351043014 -r 1e1782c1aedf src/Tools/Code/code_runtime.ML
--- 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
 
diff -r f6e351043014 -r 1e1782c1aedf src/Tools/induct.ML
--- 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