# HG changeset patch
# User bulwahn
# Date 1320047435 -3600
# Node ID 97b77157900072051cbb793acffcfbd200b4f949
# Parent  16bab9f1bb374faa29d57584daa0ad1b0d486881
clarified signature

diff -r 16bab9f1bb37 -r 97b771579000 src/HOL/Tools/Quotient/quotient_typ.ML
--- 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