diff -r 96814d676c49 -r 71a0a8687d6c src/HOL/Tools/Lifting/lifting_info.ML
--- 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