# HG changeset patch
# User kuncar
# Date 1417785276 -3600
# Node ID ec23f2a97ba40aa517c28b01453108bb264d0890
# Parent  eb4e322734bfc382960b66add39406f494d9e773
publish lifting_forget and lifting_udpate interface

diff -r eb4e322734bf -r ec23f2a97ba4 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Dec 05 14:14:36 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Dec 05 14:14:36 2014 +0100
@@ -17,6 +17,10 @@
   val setup_by_typedef_thm: config -> thm -> local_theory -> binding * local_theory
 
   val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
+
+  val lifting_forget: string -> local_theory -> local_theory
+  val update_transfer_rules: string -> local_theory -> local_theory
+  val pointer_of_bundle_binding: Proof.context -> binding -> string
 end
 
 structure Lifting_Setup: LIFTING_SETUP =
@@ -988,6 +992,9 @@
       | _ => error "The provided bundle is not a lifting bundle."
   end
 
+fun pointer_of_bundle_binding ctxt binding = Name_Space.full_name (Name_Space.naming_of 
+      (Context.Theory (Proof_Context.theory_of ctxt))) binding
+
 fun lifting_forget pointer lthy =
   let
     fun get_transfer_rules_to_delete qinfo ctxt =