# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1262304638 -3600
# Node ID 282fe9cc278eeb28711d08d57b465037c17aee30
# Parent  71225f4a46355bc66f8379fc700a844b23fdd5a1
fixed comment errors

diff -r 71225f4a4635 -r 282fe9cc278e Quot/quotient_def.ML
--- 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)
diff -r 71225f4a4635 -r 282fe9cc278e Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Jan 01 01:08:19 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 01 01:10:38 2010 +0100
@@ -64,7 +64,6 @@
 (*                                                  *)
 (* for example for: ?'a list                        *)
 (* it produces:     %a. map a                       *)
-(* 
 fun mk_mapfun ctxt vs ty =
 let
   val vs' = map (mk_Free) vs