--- a/Quot/Examples/IntEx2.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -108,7 +108,7 @@
 
 lemma mult_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
-apply(simp only: fun_rel.simps)
+apply(simp only: fun_rel_def)
 apply(rule allI | rule impI)+
 apply(rule equivp_transp[OF int_equivp])
 apply(rule mult_raw_fst)

--- a/Quot/Examples/LarryInt.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/Examples/LarryInt.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -178,7 +178,7 @@
 
 lemma [quot_respect]:
   shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
-apply(simp only: fun_rel.simps)
+apply(simp only: fun_rel_def)
 apply(rule allI | rule impI)+
 apply(rule equivp_transp[OF int_equivp])
 apply(rule mult_raw_fst)

--- a/Quot/QuotList.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/QuotList.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -74,7 +74,7 @@
 lemma cons_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
-by (simp only: expand_fun_eq fun_map.simps cons_prs_aux[OF q])
+by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q])
    (simp)
 
 lemma cons_rsp[quot_respect]:
@@ -103,7 +103,7 @@
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
-by (simp only: expand_fun_eq fun_map.simps map_prs_aux[OF a b])
+by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
    (simp)
 
 
@@ -129,7 +129,7 @@
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
-by (simp only: expand_fun_eq fun_map.simps foldr_prs_aux[OF a b])
+by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b])
    (simp)
 
 lemma foldl_prs_aux:
@@ -143,7 +143,7 @@
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
-by (simp only: expand_fun_eq fun_map.simps foldl_prs_aux[OF a b])
+by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b])
    (simp)
 
 lemma list_rel_empty: "list_rel R [] b \<Longrightarrow> length b = 0"

--- a/Quot/QuotProd.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/QuotProd.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -46,7 +46,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
-apply(simp only: expand_fun_eq fun_map.simps pair_prs_aux[OF q1 q2])
+apply(simp only: expand_fun_eq fun_map_def pair_prs_aux[OF q1 q2])
 apply(simp)
 done
 

--- a/Quot/QuotScript.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/QuotScript.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -126,30 +126,19 @@
   using a unfolding Quotient_def transp_def
   by metis
 
-fun
-  fun_map
+definition
+  fun_map (infixr "--->" 55)
 where
-  "fun_map f g h x = g (h (f x))"
-
-abbreviation
-  fun_map_syn (infixr "--->" 55)
-where
-  "f ---> g \<equiv> fun_map f g"
+[simp]: "fun_map f g h x = g (h (f x))"
 
 lemma fun_map_id:
   shows "(id ---> id) = id"
   by (simp add: expand_fun_eq id_def)
 
-
-fun
-  fun_rel
+definition
+  fun_rel (infixr "===>" 55)
 where
-  "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
-
-abbreviation
-  fun_rel_syn (infixr "===>" 55)
-where
-  "E1 ===> E2 \<equiv> fun_rel E1 E2"
+[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
 lemma fun_rel_eq:
   "(op =) ===> (op =) \<equiv> (op =)"
@@ -453,18 +442,18 @@
   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
   by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
 
-(* 2 lemmas needed for cleaning of quantifiers *)
+(* 3 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"
   shows "Ball (Respects R) ((absf ---> id) f) = All f"
-  using a unfolding Quotient_def
-  by (metis in_respects fun_map.simps id_apply)
+  using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
+by metis
 
 lemma ex_prs:
   assumes a: "Quotient R absf repf"
   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
-  using a unfolding Quotient_def
-  by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply)
+  using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
+  by metis
 
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
@@ -639,8 +628,13 @@
   and     r2: "Respects (R1 ===> R2) g" 
   shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
   apply(rule_tac iffI)
+  apply(rule)+
+  apply (rule apply_rsp'[of "R1" "R2"])
+  apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]])
+  apply auto
   using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
-  apply(metis apply_rsp')
+  apply (metis let_rsp q1)
+  apply (metis fun_rel_eq_rel let_rsp q1 q2 r2)
   using r1 unfolding Respects_def expand_fun_eq
   apply(simp (no_asm_use))
   apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])

--- a/Quot/quotient_tacs.ML	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 21 19:52:46 2010 +0100
@@ -431,7 +431,7 @@
     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
         if (member (op=) xs h)
         then Conv.all_conv ctrm
-        else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm 
+        else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm 
   | _ => Conv.all_conv ctrm
 
 fun fun_map_conv xs ctxt ctrm =