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.ML
changeset 311 77fc6f3c0343
parent 293 653460d3e849
child 312 4cf79f70efec 
--- a/quotient.ML	Thu Nov 12 02:18:36 2009 +0100
+++ b/quotient.ML	Thu Nov 12 02:54:40 2009 +0100
@@ -146,7 +146,8 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val lthy3 = quotdata_update (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
+  val lthy3 = quotdata_update (Binding.str_of qty_name) 
+                                (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
nominal2