--- a/Quot/QuotMain.thy	Sat Dec 12 15:07:59 2009 +0100
+++ b/Quot/QuotMain.thy	Sat Dec 12 15:08:25 2009 +0100
@@ -294,6 +294,16 @@
        in
          (* TODO/FIXME: This test is not enough. *) 
          (*             Why?                     *)
+(* Because constants can have the same name but not be the same
+   constant.  All overloaded constants have the same name but because
+   of different types they do differ.
+
+   This code will let one write a theorem where plus on nat is
+   matched to plus on int, even if the latter is defined differently.
+
+   This would result in hard to understand failures in injection and
+   cleaning.
+*)
          if same_name rtrm qtrm then rtrm
          else 
            let