--- a/quotient_def.ML	Wed Nov 11 10:22:47 2009 +0100
+++ b/quotient_def.ML	Wed Nov 11 18:49:46 2009 +0100
@@ -10,6 +10,7 @@
     local_theory -> (term * thm) * local_theory
   val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
     local_theory -> local_theory
+  val diff: (typ * typ) -> (typ * typ) list -> (typ * typ) list
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -176,4 +177,4 @@
 
 end; (* structure *)
 
-open Quotient_Def;
\ No newline at end of file
+open Quotient_Def;