# HG changeset patch
# User wenzelm
# Date 1519048151 -3600
# Node ID ad2b3e330c27568ecfc0b8626c63560e7be22250
# Parent  3f330245aebe33e514ae25eb3dea165c12c15b55
tuned signature;

diff -r 3f330245aebe -r ad2b3e330c27 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Mon Feb 19 14:30:06 2018 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Mon Feb 19 14:49:11 2018 +0100
@@ -276,8 +276,7 @@
 
 fun retrieve_function_data ctxt t =
   Item_Net.retrieve (get_functions ctxt) t
-  |> (map o apsnd)
-      (transform_function_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+  |> (map o apsnd) (transform_function_data (Morphism.transfer_morphism' ctxt));
 
 val add_function_data =
   transform_function_data Morphism.trim_context_morphism #>
diff -r 3f330245aebe -r ad2b3e330c27 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Feb 19 14:30:06 2018 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon Feb 19 14:49:11 2018 +0100
@@ -60,7 +60,7 @@
 
 fun lookup_mode ctxt =
   Symtab.lookup (Modes.get (Context.Proof ctxt))
-  #> Option.map (transform_setup_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+  #> Option.map (transform_setup_data (Morphism.transfer_morphism' ctxt));
 
 
 (*** Automated monotonicity proofs ***)
diff -r 3f330245aebe -r ad2b3e330c27 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon Feb 19 14:30:06 2018 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Mon Feb 19 14:49:11 2018 +0100
@@ -106,7 +106,7 @@
 
 fun lookup_quotmaps_generic context name =
   Symtab.lookup (get_quotmaps context) name
-  |> Option.map (transform_quotmaps (Morphism.transfer_morphism (Context.theory_of context)))
+  |> Option.map (transform_quotmaps (Morphism.transfer_morphism'' context))
 
 val lookup_quotmaps = lookup_quotmaps_generic o Context.Proof
 val lookup_quotmaps_global = lookup_quotmaps_generic o Context.Theory
@@ -172,7 +172,7 @@
 
 fun lookup_quotients_generic context name =
   Symtab.lookup (get_quotients context) name
-  |> Option.map (transform_quotients (Morphism.transfer_morphism (Context.theory_of context)))
+  |> Option.map (transform_quotients (Morphism.transfer_morphism'' context))
 
 val lookup_quotients = lookup_quotients_generic o Context.Proof
 val lookup_quotients_global = lookup_quotients_generic o Context.Theory
@@ -211,7 +211,7 @@
 
 fun dest_quotconsts_generic context =
   maps #2 (Symtab.dest (get_quotconsts context))
-  |> map (transform_quotconsts (Morphism.transfer_morphism (Context.theory_of context)))
+  |> map (transform_quotconsts (Morphism.transfer_morphism'' context))
 
 val dest_quotconsts = dest_quotconsts_generic o Context.Proof
 val dest_quotconsts_global = dest_quotconsts_generic o Context.Theory
diff -r 3f330245aebe -r ad2b3e330c27 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Mon Feb 19 14:30:06 2018 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML	Mon Feb 19 14:49:11 2018 +0100
@@ -868,7 +868,7 @@
   end
 
 fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
-  |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+  |> Option.map (morph_pred_data (Morphism.transfer_morphism' ctxt))
 
 fun update_pred_data type_name qinfo ctxt =
   Data.map (map_pred_data (Symtab.update (type_name, qinfo))) ctxt
diff -r 3f330245aebe -r ad2b3e330c27 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Feb 19 14:30:06 2018 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Feb 19 14:49:11 2018 +0100
@@ -257,14 +257,14 @@
 fun the_inductive ctxt term =
   Item_Net.retrieve (#infos (rep_data ctxt)) term
   |> the_single
-  |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+  |> apsnd (transform_result (Morphism.transfer_morphism' ctxt))
 
 fun the_inductive_global ctxt name =
   #infos (rep_data ctxt)
   |> Item_Net.content
   |> filter (fn ({names, ...}, _) => member op = names name)
   |> the_single
-  |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+  |> apsnd (transform_result (Morphism.transfer_morphism' ctxt))
 
 fun put_inductives info =
   map_data (fn (infos, monos, equations) =>
diff -r 3f330245aebe -r ad2b3e330c27 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Feb 19 14:30:06 2018 +0100
+++ b/src/HOL/Tools/typedef.ML	Mon Feb 19 14:49:11 2018 +0100
@@ -72,7 +72,7 @@
 
 fun get_info_generic context =
   Symtab.lookup_list (Data.get context) #>
-  map (transform_info (Morphism.transfer_morphism (Context.theory_of context)));
+  map (transform_info (Morphism.transfer_morphism'' context));
 
 val get_info = get_info_generic o Context.Proof;
 val get_info_global = get_info_generic o Context.Theory;
diff -r 3f330245aebe -r ad2b3e330c27 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Feb 19 14:30:06 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Feb 19 14:49:11 2018 +0100
@@ -468,7 +468,7 @@
   |> Context_Position.set_visible_generic false
   |> pair (Idents.get context)
   |> roundup (Context.theory_of context)
-      (activate_notes Element.init' (Morphism.transfer_morphism o Context.theory_of) context export)
+      (activate_notes Element.init' Morphism.transfer_morphism'' context export)
       (the_default Morphism.identity export) dep
   |-> Idents.put
   |> Context_Position.restore_visible_generic context;
@@ -481,7 +481,7 @@
     context
     |> Context_Position.set_visible_generic false
     |> pair empty_idents
-    |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of)
+    |> activate_all name thy Element.init' Morphism.transfer_morphism''
     |-> (fn marked' => Idents.put (merge_idents (marked, marked')))
     |> Context_Position.restore_visible_generic context
     |> Context.proof_of
diff -r 3f330245aebe -r ad2b3e330c27 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Mon Feb 19 14:30:06 2018 +0100
+++ b/src/Pure/morphism.ML	Mon Feb 19 14:49:11 2018 +0100
@@ -39,6 +39,8 @@
   val fact_morphism: string -> (thm list -> thm list) -> morphism
   val thm_morphism: string -> (thm -> thm) -> morphism
   val transfer_morphism: theory -> morphism
+  val transfer_morphism': Proof.context -> morphism
+  val transfer_morphism'': Context.generic -> morphism
   val trim_context_morphism: morphism
   val instantiate_morphism:
     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism
@@ -120,6 +122,9 @@
 fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
 
 val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
+val transfer_morphism' = transfer_morphism o Proof_Context.theory_of;
+val transfer_morphism'' = transfer_morphism o Context.theory_of;
+
 val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
 
 fun instantiate_morphism ([], []) = identity