--- a/Quot/QuotMain.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -398,21 +398,25 @@
        in 
          if rel' = rel then rtrm else raise exc
        end  
-  | (_, Const (s, _)) =>
+  | (_, Const (s, Type(st, _))) =>
        let 
          fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
            | same_name _ _ = false
        in
-         if same_name rtrm qtrm 
-         then rtrm 
+         (* TODO/FIXME: This test is not enough *)
+         if same_name rtrm qtrm then rtrm
          else 
            let 
-             fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)")
-             val exc2   = LIFT_MATCH ("regularize (constant mismatch)")
+             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 rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) 
+             val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
            in 
-             if matches_term (rtrm, rtrm') then rtrm else raise exc2
+             if matches_term (rtrm, rtrm') then rtrm else
+               let
+                 val _ = tracing (Syntax.string_of_term @{context} rtrm);
+                 val _ = tracing (Syntax.string_of_term @{context} rtrm');
+               in raise exc2 end
            end
        end 
 
@@ -616,6 +620,7 @@
   | (_, Const (@{const_name "op ="}, _)) => rtrm
 
     (* FIXME: check here that rtrm is the corresponding definition for the const *)
+    (* Hasn't it already been checked in regularize? *)
   | (_, Const (_, T')) =>
       let
         val rty = fastype_of rtrm