--- a/QuotMain.thy	Thu Oct 22 13:45:48 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 15:02:01 2009 +0200
@@ -1092,32 +1092,9 @@
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
-ML_prf {*
-  val concl = (#concl o fst) (Subgoal.focus @{context} 1 (Isar.goal ()));
-  val pat = Drule.strip_imp_concl (cprop_of @{thm RES_FORALL_RSP});
-  val ((_,p),(_,c)) = (Thm.dest_comb pat, Thm.dest_comb concl);
-  val ((_,p),(_,c)) = (Thm.dest_comb p, Thm.dest_comb c);
-*}
-ML_prf {*
-  val ((_,pn),(_,cn)) = (Thm.dest_comb p, Thm.dest_comb c);
-  val (pnm, cnm) = (@{cpat "?a"}, @{cterm "b::('a List.list \<Rightarrow> bool)"});
-  val (pp, cc) = (term_of pn, term_of cn);
-  val (ppt, cct) = (type_of pp, type_of cc);
-  val (ppm, ccm) = (term_of pnm, term_of cnm);
-  val i = Pattern.first_order_match @{theory} (ppm, ccm) (Vartab.empty, Vartab.empty);
-  val (ppmt, ccmt) = (type_of ppm, type_of ccm);
-  val ii = Sign.typ_match @{theory} (ppmt, cct) (Vartab.empty);
-  val ii = Sign.typ_match @{theory} (ppt, cct) (Vartab.empty);
-*}
-.
-  val pat = Drule.strip_imp_concl (cprop_of thm)
-  val insts = Thm.match (pat, concl)
-
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-thm RES_FORALL_RSP
-apply (rule_tac RES_FORALL_RSP)
-
-prefer 2
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (simp only: FUN_REL.simps)
 (* ABS_REP_RSP *)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RSP *)
@@ -1168,11 +1145,16 @@
 apply (assumption)
 apply (simp)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-prefer 2
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-prefer 2
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (simp only: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
@@ -1184,7 +1166,14 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp add: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-sorry
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (simp only: FUN_REL.simps)
+done
 
 prove list_induct_t: trm
 apply (simp only: list_induct_tr[symmetric])

--- a/QuotScript.thy	Thu Oct 22 13:45:48 2009 +0200
+++ b/QuotScript.thy	Thu Oct 22 15:02:01 2009 +0200
@@ -474,7 +474,7 @@
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
 lemma RES_FORALL_RSP:
-  assumes a: "QUOTIENT R abs rep"
+  assumes a: "QUOTIENT R absf repf"
   shows "\<And>f g. (R ===> (op =)) f g ==>
         (Ball (Respects R) f = Ball (Respects R) g)"
   sorry