--- 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 #>
--- 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 ***)
--- 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
--- 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
--- 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) =>
--- 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;
--- 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
--- 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