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