--- a/quotient.ML	Sun Nov 22 00:01:06 2009 +0100
+++ b/quotient.ML	Sun Nov 22 15:30:23 2009 +0100
@@ -18,7 +18,7 @@
 fun define (name, mx, rhs) lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
-     Local_Theory.define "" ((name, mx), (Attrib.empty_binding, rhs)) lthy
+     Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
 in
   ((rhs, thm), lthy')
 end