diff -r 1a0f0b758071 -r 345c422b1cb5 quotient.ML
--- 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