--- a/Quot/quotient_def.ML	Mon Feb 15 12:23:02 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Feb 15 13:40:03 2010 +0100
@@ -11,7 +11,7 @@
     local_theory -> (term * thm) * local_theory
 
   val quotdef_cmd: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) ->
-    local_theory -> local_theory
+    local_theory -> (term * thm) * local_theory
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -70,7 +70,7 @@
   val lthy' = Variable.declare_term lhs lthy
   val lthy'' = Variable.declare_term rhs lthy'
 in
-  quotient_def (bindmx, (attr, (lhs, rhs))) lthy'' |> snd
+  quotient_def (bindmx, (attr, (lhs, rhs))) lthy''
 end
 
 val binding_mixfix_parser = OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where"
@@ -81,6 +81,6 @@
 val _ =
   OuterSyntax.local_theory "quotient_definition"
     "definition for constants over the quotient type"
-      OuterKeyword.thy_decl (quotdef_parser >> (quotdef_cmd))
+      OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
 
 end; (* structure *)