--- a/src/HOL/Tools/Quotient/quotient_typ.ML Mon Oct 31 08:43:21 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Mon Oct 31 08:50:35 2011 +0100
@@ -7,7 +7,7 @@
signature QUOTIENT_TYPE =
sig
val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
- -> Proof.context -> Quotient_Info.quotients * local_theory
+ -> local_theory -> Quotient_Info.quotients * local_theory
val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
-> Proof.context -> Proof.state