--- a/src/HOL/Tools/Function/function_common.ML Sun Feb 18 16:31:56 2018 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Sun Feb 18 17:57:14 2018 +0100
@@ -306,25 +306,13 @@
termination : thm,
domintros : thm list option}
-fun lift_morphism ctxt f =
- let
- fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of ctxt t))
- in
- Morphism.morphism "lift_morphism"
- {binding = [],
- typ = [Logic.type_map term],
- term = [term],
- fact = [map f]}
- end
-
fun import_function_data t ctxt =
let
val ct = Thm.cterm_of ctxt t
- val inst_morph = lift_morphism ctxt o Thm.instantiate
-
- fun match (trm, data) =
- SOME (transform_function_data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))) data)
- handle Pattern.MATCH => NONE
+ fun inst_morph u =
+ Morphism.instantiate_morphism (Thm.match (Thm.cterm_of ctxt u, ct))
+ fun match (u, data) =
+ SOME (transform_function_data (inst_morph u) data) handle Pattern.MATCH => NONE
in
get_first match (retrieve_function_data ctxt t)
end
--- a/src/Pure/morphism.ML Sun Feb 18 16:31:56 2018 +0100
+++ b/src/Pure/morphism.ML Sun Feb 18 17:57:14 2018 +0100
@@ -40,6 +40,8 @@
val thm_morphism: string -> (thm -> thm) -> morphism
val transfer_morphism: theory -> morphism
val trim_context_morphism: morphism
+ val instantiate_morphism:
+ ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism
end;
structure Morphism: MORPHISM =
@@ -120,6 +122,19 @@
val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
+fun instantiate_morphism ([], []) = identity
+ | instantiate_morphism (cinstT, cinst) =
+ let
+ val instT = map (apsnd Thm.typ_of) cinstT;
+ val inst = map (apsnd Thm.term_of) cinst;
+ in
+ morphism "instantiate"
+ {binding = [],
+ typ = if null instT then [] else [Term_Subst.instantiateT instT],
+ term = [Term_Subst.instantiate (instT, inst)],
+ fact = [map (Thm.instantiate (cinstT, cinst))]}
+ end;
+
end;
structure Basic_Morphism: BASIC_MORPHISM = Morphism;