src/Pure/morphism.ML
changeset 67651 6dd41193a72a
parent 67650 5e4f9a0ffea5
child 67664 ad2b3e330c27
--- 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;