diff -r f7cafd3c86b0 -r 4f5512569468 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 20 12:33:19 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 20 16:44:31 2010 +0100
@@ -435,9 +435,10 @@
   | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
        in
-         if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
-         then term_mismatch "regularize(ball)" ctxt rtrm qtrm
+         if resrel <> needrel
+         then term_mismatch "regularize(ball)" ctxt resrel needrel
          else mk_ball $ (mk_resp $ resrel) $ subtrm
        end
 
@@ -452,9 +453,10 @@
   | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
        in
-         if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
-         then term_mismatch "regularize(bex)" ctxt rtrm qtrm
+         if resrel <> needrel
+         then term_mismatch "regularize(bex)" ctxt resrel needrel
          else mk_bex $ (mk_resp $ resrel) $ subtrm
        end