diff -r 2d9de77d5687 -r 0dd10a900cae Quot/QuotMain.thy --- 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