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.
Quot/quotient_def.ML
changeset 801 282fe9cc278e
parent 800 71225f4a4635
child 804 ba7e81531c6d 
--- a/Quot/quotient_def.ML	Fri Jan 01 01:08:19 2010 +0100
+++ b/Quot/quotient_def.ML	Fri Jan 01 01:10:38 2010 +0100
@@ -38,7 +38,7 @@
 
 fun quotient_def mx attr lhs rhs lthy =
 let
-  val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.)
+  val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
   val qconst_bname = Binding.name lhs_str;
   val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, absrep_trm)
nominal2