--- 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 *)
--- 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;