Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
quotient_def.ML
changeset 331 345c422b1cb5
parent 329 5d06e1dba69a
child 365 ba057402ea53 
--- 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
nominal2