# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260627838 -3600
# Node ID f48b8a82c1e39976da1306e83a9ba19bcce1dfc5
# Parent  214b8c35b24420108dc59c4b7daab665f670491f
tried to improve test; but fails

diff -r 214b8c35b244 -r f48b8a82c1e3 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sat Dec 12 15:08:25 2009 +0100
+++ b/Quot/QuotMain.thy	Sat Dec 12 15:23:58 2009 +0100
@@ -287,29 +287,30 @@
          if rel' = rel then rtrm else raise exc
        end  
 
-  | (_, Const (s, Type(st, _))) =>
+  | (_, Const _) =>
        let 
-         fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
+         fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)
            | same_name _ _ = false
+          (* 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. *)
+           (* cu: if I also test the type, then something else breaks *)
        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 
-             val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)")
-             val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)")
              val thy = ProofContext.theory_of lthy
+             val qtrm_str = Syntax.string_of_term lthy qtrm
+             val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
+             val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
              val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
            in 
              if Pattern.matches thy (rtrm', rtrm)