# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260273636 -3600
# Node ID c4299ce27e46318e59e5d57c32b907747c050e1e
# Parent  280c12bde1c49783f9f174b121a4dabee9f6d5bd
Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned

diff -r 280c12bde1c4 -r c4299ce27e46 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 12:59:38 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 13:00:36 2009 +0100
@@ -874,25 +874,14 @@
           (resolve_tac trans2 THEN' RANGE [
             quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*)
 
-(* TODO: These patterns should should be somehow combined and generalized... *)
-| (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_name prod_rel}, _) $ _ $ _) $
-    (Const (@{const_name prod_rel}, _) $ _ $ _)
-    => rtac @{thm quot_rel_rsp} 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
+| _ $ _ $ _
+    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) ORELSE' rep_abs_rsp_tac ctxt
 
 | _ => error "inj_repabs_tac not a relation"
 ) i)