--- a/QuotMain.thy	Fri Dec 04 15:25:51 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 15:41:09 2009 +0100
@@ -143,7 +143,7 @@
 
 declare [[map list = (map, LIST_REL)]]
 declare [[map * = (prod_fun, prod_rel)]]
-declare [[map "fun" = (fun_map, FUN_REL)]]
+declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quotient_thm] = 
   FUN_Quotient LIST_Quotient
@@ -540,7 +540,7 @@
   in
   case redex of
       (ogl as ((Const (@{const_name "Ball"}, _)) $
-        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
+        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
       (let
         val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
@@ -571,7 +571,7 @@
   in
   case redex of
       (ogl as ((Const (@{const_name "Bex"}, _)) $
-        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
+        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
       (let
         val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
@@ -728,37 +728,11 @@
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
-lemma FUN_REL_I:
+lemma fun_rel_id:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   shows "(R1 ===> R2) f g"
 using a by simp
 
-ML {*
-val lambda_rsp_tac =
-  SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
-       (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i
-     | _ => no_tac)
-*}
-
-ML {*
-val ball_rsp_tac = 
-  SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
-        (_ $ (Const (@{const_name Ball}, _) $ _) 
-           $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i
-      |_ => no_tac)
-*}
-
-ML {*
-val bex_rsp_tac = 
-  SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
-        (_ $ (Const (@{const_name Bex}, _) $ _) 
-           $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i
-      | _ => no_tac)
-*}
-
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -936,28 +910,28 @@
 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
     (* (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_I} THEN' quot_true_tac ctxt unlam
+  ((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 fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+      => 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 fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+      => 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'