--- a/QuotMain.thy	Sun Dec 06 11:09:51 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 11:21:29 2009 +0100
@@ -269,6 +269,7 @@
        else false
   | _ => false
 *}
+
 ML {*
 fun matches_term (trm, trm') = 
    case (trm, trm') of 
@@ -954,42 +955,51 @@
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
   ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+
     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 | (Const (@{const_name "op ="},_) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+
     (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+
     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 | Const (@{const_name "op ="},_) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+
     (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
-| Const (@{const_name "op ="},_) $ _ $ _ => 
+
     (* reflexivity of operators arising from Cong_tac *)
-    rtac @{thm refl} ORELSE'
-    (resolve_tac trans2 THEN' RANGE [
-      quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+| Const (@{const_name "op ="},_) $ _ $ _ 
+      => rtac @{thm refl} ORELSE'
+          (resolve_tac trans2 THEN' RANGE [
+            quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const (@{const_name fun_rel}, _) $ _ $ _)
     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
-| _ $ (Const _) $ (Const _) => (* fun_rel, list_rel, etc but not equality *)
-    (* respectfulness of constants; in particular of a simple relation *)
-    resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
-| _ $ _ $ _ =>
+
+   (* respectfulness of constants; in particular of a simple relation *)
+| _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
+    => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *)
-    rep_abs_rsp_tac ctxt
+| _ $ _ $ _ 
+    => rep_abs_rsp_tac ctxt
+
 | _ => error "inj_repabs_tac not a relation"
 ) i)
 *}