# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260626254 -3600
# Node ID 0b5b6850c48394713c531125ceee04b7bcc757a9
# Parent  33cd648df179913428abb9216d8f79fd0a20034c
Answering the question in code.

diff -r 33cd648df179 -r 0b5b6850c483 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sat Dec 12 13:54:01 2009 +0100
+++ b/Quot/QuotMain.thy	Sat Dec 12 14:57:34 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