--- a/FSet.thy	Sat Nov 28 08:46:24 2009 +0100
+++ b/FSet.thy	Sat Nov 28 13:54:48 2009 +0100
@@ -328,9 +328,11 @@
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 done
 
-lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) =
+ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+
+lemma "FOLD f g (z::'b) (INSERT a x) =
   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
-apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
+apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
@@ -341,8 +343,6 @@
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done
 
-ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
-
 lemma cheat: "P" sorry
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"

--- a/QuotMain.thy	Sat Nov 28 08:46:24 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 13:54:48 2009 +0100
@@ -488,6 +488,7 @@
 
 *)
 
+(* FIXME: they should be in in the new Isabelle *)
 lemma [mono]: 
   "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
 by blast
@@ -811,7 +812,7 @@
 using a by (simp add: FUN_REL.simps)
 
 ML {*
-val LAMBDA_RES_TAC =
+val lambda_res_tac =
   Subgoal.FOCUS (fn {concl, ...} =>
     case (term_of concl) of
        (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1
@@ -819,7 +820,7 @@
 *}
 
 ML {*
-val WEAK_LAMBDA_RES_TAC =
+val weak_lambda_res_tac =
   Subgoal.FOCUS (fn {concl, ...} =>
     case (term_of concl) of
        (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1
@@ -831,7 +832,8 @@
 val ball_rsp_tac = 
   Subgoal.FOCUS (fn {concl, ...} =>
      case (term_of concl) of
-        (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) =>
+        (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) 
+                $ (Const (@{const_name Ball}, _) $ _))) =>
             rtac @{thm FUN_REL_I} 1
       |_ => no_tac)
 *}
@@ -840,7 +842,8 @@
 val bex_rsp_tac = 
   Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
      case (term_of concl) of
-        (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) =>
+        (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) 
+                $ (Const (@{const_name Bex}, _) $ _))) =>
             rtac @{thm FUN_REL_I} 1
       | _ => no_tac)
 *}
@@ -877,7 +880,7 @@
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
-           LAMBDA_RES_TAC ctxt,
+           lambda_res_tac ctxt,
            rtac @{thm RES_FORALL_RSP},
            ball_rsp_tac ctxt,
            rtac @{thm RES_EXISTS_RSP},
@@ -892,8 +895,8 @@
            rtac @{thm ext},
            resolve_tac rel_refl,
            atac,
-           SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
-           WEAK_LAMBDA_RES_TAC ctxt,
+           (*seems not necessary:: SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),*)
+           weak_lambda_res_tac ctxt,
            CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))])
 
 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
@@ -905,7 +908,7 @@
 we try:
 
  1) theorems 'trans2' from the appropriate QUOT_TYPE
- 2) remove lambdas from both sides: LAMBDA_RES_TAC
+ 2) remove lambdas from both sides: lambda_res_tac
  3) remove Ball/Bex from the right hand side
  4) use user-supplied RSP theorems
  5) remove rep_abs from the right side
@@ -929,11 +932,11 @@
     (K (print_tac "start")) THEN' (K no_tac), 
   
     (* "cong" rule of the of the relation    *)
-    (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *)
+    (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> a \<approx> b = c \<approx> d *)
     DT ctxt "1" (resolve_tac trans2),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    DT ctxt "2" (LAMBDA_RES_TAC ctxt),
+    DT ctxt "2" (lambda_res_tac ctxt),
 
     (* = (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
     DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
@@ -947,7 +950,7 @@
     (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
     DT ctxt "6" (bex_rsp_tac ctxt),
 
-    (* respectfulness of ops *)
+    (* respectfulness of constants *)
     DT ctxt "7" (resolve_tac rsp_thms),
 
     (* reflexivity of operators arising from Cong_tac *)
@@ -974,39 +977,17 @@
     (* resolving with R x y assumptions *)
     DT ctxt "E" (atac),
 
-    DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
-    DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
+    (* seems not necessay:: DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*)
+    DT ctxt "G" (weak_lambda_res_tac ctxt),
+
+    (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed to apply respectfulness theorems *)
+    (* works globally *)
     DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))])
 
 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
   REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
-ML {*
-fun get_inj_repabs_tac ctxt rel lhs rhs =
-let
-  val _ = tracing "input"
-  val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel)
-  val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs)
-  val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs)
-in  
-  case (rel, lhs, rhs) of
-    (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *)
-      => rtac @{thm REP_ABS_RSP(1)}
-  | (_, Const (@{const_name "Ball"}, _) $ _, 
-        Const (@{const_name "Ball"}, _) $ _)
-      => rtac @{thm RES_FORALL_RSP}
-  | _ => K no_tac
-end
-*}
-
-ML {* 
-fun inj_repabs_tac ctxt =
-  SUBGOAL (fn (goal, i) =>
-     (case (HOLogic.dest_Trueprop goal) of
-        (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs
-      | _ => K no_tac) i)
-*}
 
 section {* Cleaning of the theorem *}