# HG changeset patch
# User wenzelm
# Date 1519405197 -3600
# Node ID 3c9e0b4709e789262964ce2bd42b4bfd113a903e
# Parent  f7e37a94caee1d60bfaeac81f36b96e24bb261b0
tuned -- use existing Morphism.instantiate_morphism;

diff -r f7e37a94caee -r 3c9e0b4709e7 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Feb 23 15:17:51 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Feb 23 17:59:57 2018 +0100
@@ -114,8 +114,14 @@
 fun mk_lift_const_of_lift_def qty lift_def = Envir.subst_term_types (mk_inst_of_lift_def qty lift_def)
   (lift_const_of_lift_def lift_def)
 
-fun inst_of_lift_def ctxt qty lift_def =  mk_inst_of_lift_def qty lift_def
-  |> instT_morphism ctxt |> (fn phi => morph_lift_def phi lift_def)
+fun inst_of_lift_def ctxt qty lift_def =
+  let
+    val instT =
+      Vartab.fold (fn (a, (S, T)) => cons ((a, S), Thm.ctyp_of ctxt T))
+        (mk_inst_of_lift_def qty lift_def) []
+    val phi = Morphism.instantiate_morphism (instT, [])
+  in morph_lift_def phi lift_def end
+
 
 (* Config *)
 
diff -r f7e37a94caee -r 3c9e0b4709e7 src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Fri Feb 23 15:17:51 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Fri Feb 23 17:59:57 2018 +0100
@@ -33,8 +33,6 @@
   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
   val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory
 end
 
@@ -138,21 +136,6 @@
     map_interrupt' f l []
   end
 
-fun instT_thm ctxt env =
-  let
-    val cinst = env |> Vartab.dest 
-      |> map (fn (x, (S, T)) => ((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)]};
-
 fun conceal_naming_result f lthy = 
   let val old_lthy = lthy
   in lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming old_lthy end;