Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated to Isabelle 22nd November
authorChristian Urban <urbanc@in.tum.de>
Sun, 22 Nov 2009 15:30:23 +0100
changeset 331 345c422b1cb5
parent 330 1a0f0b758071
child 332 87f5fbebd6d5
updated to Isabelle 22nd November
quotient.ML file | annotate | diff | comparison | revisions
quotient_def.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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