--- 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