src/HOL/Tools/Lifting/lifting_setup.ML

     binding * local_theory
 
   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 =
 struct
 

             handle ERROR _ => error "The provided bundle is not a lifting bundle."
         in name end
       | _ => 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 =
       let
         val transfer_rel = get_transfer_rel qinfo