# HG changeset patch
# User kuncar
# Date 1416323997 -3600
# Node ID b614363356eda6bbadac543e161c2806e01ea4e3
# Parent  78fc1b798c61563ae69a8b7a55be03b3ebe924ec
useful function

diff -r 78fc1b798c61 -r b614363356ed src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Tue Nov 18 16:19:57 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Tue Nov 18 16:19:57 2014 +0100
@@ -32,6 +32,8 @@
   val mk_HOL_eq: thm -> thm
   val safe_HOL_meta_eq: thm -> thm
   val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option
+  val instT_thm: Proof.context -> Type.tyenv -> thm -> thm
+  val instT_morphism: Proof.context -> Type.tyenv -> morphism
 end
 
 
@@ -132,4 +134,19 @@
     map_interrupt' f l []
   end
 
+fun instT_thm ctxt env =
+  let
+    val cinst = env |> Vartab.dest 
+      |> map (fn (x, (S, T)) => (Thm.ctyp_of ctxt (TVar (x, S)), Thm.ctyp_of ctxt T));
+  in
+    Thm.instantiate (cinst, [])
+  end;
+
+fun instT_morphism ctxt env =
+  Morphism.morphism "Lifting_Util.instT"
+    {binding = [],
+    typ = [Envir.subst_type env],
+    term = [Envir.subst_term_types env],
+    fact = [map (instT_thm ctxt env)]};
+
 end