diff -r fb4bfbb1a291 -r a31cf260eeb3 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Sat Dec 26 08:06:45 2009 +0100
+++ b/Quot/quotient_info.ML	Sat Dec 26 09:03:35 2009 +0100
@@ -13,7 +13,6 @@
   val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
   val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
-  val quotdata_dest: theory -> quotdata_info list
   val print_quotinfo: Proof.context -> unit
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}