diff -r d641c32855f0 -r 41500cd131dc QuotMain.thy
--- a/QuotMain.thy	Sat Dec 05 21:50:31 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 22:05:09 2009 +0100
@@ -149,7 +149,7 @@
   fun_quotient list_quotient
 
 lemmas [quotient_rsp] =
-  quot_rel_rsp
+  quot_rel_rsp nil_rsp cons_rsp
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
@@ -984,13 +984,6 @@
     (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 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_name fun_rel}, _) $ _ $ _) $ (Const _) $ (Const _) =>
-    (* respectfulness of constants; in particular of a simple relation *)
-    resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
 | Const (@{const_name "op ="},_) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
@@ -1005,6 +998,13 @@
     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
 | _ $ _ $ _ =>
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *)