--- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Sep 16 11:54:57 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Sep 16 11:54:57 2013 +0200
@@ -15,6 +15,7 @@
val transform_quotient: morphism -> quotient -> quotient
val lookup_quotients: Proof.context -> string -> quotient option
val update_quotients: string -> quotient -> Context.generic -> Context.generic
+ val delete_quotients: thm -> Context.generic -> Context.generic
val print_quotients: Proof.context -> unit
val get_invariant_commute_rules: Proof.context -> thm list