--- a/Quot/quotient_def.ML	Tue Dec 22 21:06:46 2009 +0100
+++ b/Quot/quotient_def.ML	Tue Dec 22 21:16:11 2009 +0100
@@ -2,7 +2,7 @@
 signature QUOTIENT_DEF =
 sig 
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
-    Proof.context -> (term * thm) * local_theory
+    local_theory -> (term * thm) * local_theory
   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
     local_theory -> local_theory
 end;