publish lifting_forget and lifting_udpate interface
authorkuncar
Fri, 05 Dec 2014 14:14:36 +0100
changeset 60226 ec23f2a97ba4
parent 60225 eb4e322734bf
child 60227 eacf75e4da95
publish lifting_forget and lifting_udpate interface
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 =