src/Pure/morphism.ML
changeset 67698 67caf783b9ee
parent 67664 ad2b3e330c27
child 69062 5eda37c06f42
--- a/src/Pure/morphism.ML	Wed Feb 21 18:37:04 2018 +0100
+++ b/src/Pure/morphism.ML	Wed Feb 21 18:41:41 2018 +0100
@@ -42,6 +42,8 @@
   val transfer_morphism': Proof.context -> morphism
   val transfer_morphism'': Context.generic -> morphism
   val trim_context_morphism: morphism
+  val instantiate_frees_morphism:
+    ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
   val instantiate_morphism:
     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism
 end;
@@ -127,6 +129,22 @@
 
 val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
 
+
+(* instantiate *)
+
+fun instantiate_frees_morphism ([], []) = identity
+  | instantiate_frees_morphism (cinstT, cinst) =
+      let
+        val instT = map (apsnd Thm.typ_of) cinstT;
+        val inst = map (apsnd Thm.term_of) cinst;
+      in
+        morphism "instantiate_frees"
+          {binding = [],
+           typ = if null instT then [] else [Term_Subst.instantiateT_frees instT],
+           term = [Term_Subst.instantiate_frees (instT, inst)],
+           fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
+      end;
+
 fun instantiate_morphism ([], []) = identity
   | instantiate_morphism (cinstT, cinst) =
       let