# HG changeset patch
# User wenzelm
# Date 1518973034 -3600
# Node ID 6dd41193a72aca99343b36a56a59ef3e00d4f56d
# Parent  5e4f9a0ffea5a9ee37bb80da1dc67377f81c07f5
more explicit instantiate_morphism (without checks for typ / term component);

diff -r 5e4f9a0ffea5 -r 6dd41193a72a src/HOL/Tools/Function/function_common.ML
--- 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
diff -r 5e4f9a0ffea5 -r 6dd41193a72a src/Pure/morphism.ML
--- 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;