diff -r 0288dd5b7ed4 -r 1610de61c44b QuotMain.thy
--- 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])