--- a/Quot/quotient_term.ML	Fri Jan 15 12:17:30 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 15 15:51:25 2010 +0100
@@ -378,15 +378,14 @@
     (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
   | _ => f (trm1, trm2)
 
-fun relation_error ctxt r1 r2 =
+fun term_mismatch str ctxt t1 t2 =
 let
-  val r1_str = Syntax.string_of_term ctxt r1
-  val r2_str = Syntax.string_of_term ctxt r2
-  val r1_ty_str = Syntax.string_of_typ ctxt (fastype_of r1)
-  val r2_ty_str = Syntax.string_of_typ ctxt (fastype_of r2)
+  val t1_str = Syntax.string_of_term ctxt t1
+  val t2_str = Syntax.string_of_term ctxt t2
+  val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
+  val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
 in
-  raise LIFT_MATCH 
-    (cat_lines ["regularise (relation mismatch)", r1_str ^ "::" ^ r1_ty_str, r2_str ^ "::" ^ r2_ty_str])
+  raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
 end
 
 (* the major type of All and Ex quantifiers *)
@@ -433,6 +432,15 @@
          else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
+  | (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')
+       in
+         if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         then term_mismatch "regularize(ball)" ctxt rtrm qtrm
+         else mk_ball $ (mk_resp $ resrel) $ subtrm
+       end
+
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -441,6 +449,15 @@
          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
+  | (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')
+       in
+         if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         then term_mismatch "regularize(bex)" ctxt rtrm qtrm
+         else mk_bex $ (mk_resp $ resrel) $ subtrm
+       end
+
   | (* equalities need to be replaced by appropriate equivalence relations *) 
     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
          if ty = ty' then rtrm
@@ -452,7 +469,7 @@
          val rel_ty = fastype_of rel
          val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') 
        in
-         if rel' aconv rel then rtrm else relation_error ctxt rel rel'
+         if rel' aconv rel then rtrm else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
        end
 
   | (_, Const _) =>
@@ -464,13 +481,11 @@
          if same_const rtrm qtrm then rtrm
          else
            let
-             val qtrm_str = Syntax.string_of_term ctxt 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) 
-             then rtrm else raise exc2
+             val rtrm' = #rconst (qconsts_lookup thy qtrm)
+               handle NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
+           in
+             if Pattern.matches thy (rtrm', rtrm)
+             then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
            end
        end