# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260626905 -3600
# Node ID 214b8c35b24420108dc59c4b7daab665f670491f
# Parent  ac2ed047988d1b5504995623f7c7707875d7a0ca# Parent  0b5b6850c48394713c531125ceee04b7bcc757a9
merged

diff -r ac2ed047988d -r 214b8c35b244 Quot/QuotMain.thy
--- 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