diff -r be0491d86d19 -r d0153a0a9b2b src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Aug 29 19:22:48 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Aug 29 20:15:13 2013 +0200
@@ -179,7 +179,7 @@
     val (_, qtyp) = quot_thm_rty_qty quot_thm
     val qty_full_name = (fst o dest_Type) qtyp
     val symtab = get_quotients' ctxt
-    fun compare_data (_, data) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
+    fun compare_data (_, data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
   in
     if Symtab.member compare_data symtab (qty_full_name, quot_thm)
       then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt