# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258900223 -3600
# Node ID 345c422b1cb5d18da2edab3c2f7670965c2e6215
# Parent  1a0f0b758071a155880c7091b5b8ae247f7f6740
updated to Isabelle 22nd November

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
diff -r 1a0f0b758071 -r 345c422b1cb5 quotient_def.ML
--- a/quotient_def.ML	Sun Nov 22 00:01:06 2009 +0100
+++ b/quotient_def.ML	Sun Nov 22 15:30:23 2009 +0100
@@ -19,7 +19,7 @@
 fun define name mx attr rhs lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
-     Local_Theory.define "" ((name, mx), (attr, rhs)) lthy
+     Local_Theory.define ((name, mx), (attr, rhs)) lthy
 in
   ((rhs, thm), lthy')
 end