# HG changeset patch
# User kuncar
# Date 1416323997 -3600
# Node ID e759afe46a8cef848809fd3e98c184b4a80b2107
# Parent  b614363356eda6bbadac543e161c2806e01ea4e3
export the result of lifting_def

diff -r b614363356ed -r e759afe46a8c src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Nov 18 16:19:57 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Nov 18 16:19:57 2014 +0100
@@ -16,6 +16,9 @@
   val abs_eq_of_lift_def: lift_def -> thm
   val rep_eq_of_lift_def: lift_def -> thm option
   val transfer_rules_of_lift_def: lift_def -> thm list
+  val morph_lift_def: morphism -> lift_def -> lift_def
+  val inst_of_lift_def: Proof.context -> typ -> lift_def -> lift_def
+  val mk_lift_const_of_lift_def: typ -> lift_def -> term
 
   val generate_parametric_transfer_rule:
     Proof.context -> thm -> thm -> thm
@@ -70,6 +73,31 @@
             def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq,
             transfer_rules = transfer_rules };
 
+fun map_lift_def f1 f2 f3 f4 f5 f6 f7 f8 f9
+  (LIFT_DEF {rty = rty, qty = qty, rhs = rhs, lift_const = lift_const,
+  def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq, 
+  transfer_rules = transfer_rules }) =
+  LIFT_DEF {rty = f1 rty, qty = f2 qty, rhs = f3 rhs, lift_const = f4 lift_const,
+            def_thm = f5 def_thm, rsp_thm = f6 rsp_thm, abs_eq = f7 abs_eq, rep_eq = f8 rep_eq,
+            transfer_rules = f9 transfer_rules }
+
+fun morph_lift_def phi =
+  let
+    val mtyp = Morphism.typ phi
+    val mterm = Morphism.term phi
+    val mthm = Morphism.thm phi
+  in
+    map_lift_def mtyp mtyp mterm mterm mthm mthm mthm (Option.map mthm) (map mthm)
+  end
+
+fun mk_inst_of_lift_def qty lift_def = Vartab.empty |> Type.raw_match (qty_of_lift_def lift_def, qty)
+
+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)
+
 (* Reflexivity prover *)
 
 fun mono_eq_prover ctxt prop =
@@ -529,7 +557,8 @@
             SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm])
             | NONE => I)
       |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
-      |> pair lift_def
+      |> ` (fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def)
+      ||> Local_Theory.restore
   end
 
 local