--- a/QuotMain.thy	Sat Oct 17 10:07:52 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 10:40:54 2009 +0200
@@ -1275,16 +1275,40 @@
   val man_inst =
     Drule.instantiate' [SOME @{ctyp 'a}, SOME @{ctyp bool}] 
       [
-       SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). y"},
-       SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (ABS_fset ---> id) ((REP_fset ---> id) x)"},
+       SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). x"},
+       SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (ABS_fset ---> id) ((REP_fset ---> id) y)"},
        SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). ([]::'a list)"},
        SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (REP_fset (ABS_fset ([]::'a list)))"}
       ] t
 *}
+ML_prf {*
+  val (tc') = (Logic.strip_assums_concl (prop_of man_inst));
+  val ps = Logic.strip_params (prop_of man_inst)
+  val tt = Term.list_abs (ps, tc')
+  val ct = cterm_of @{theory} tt
+*}
+ML_prf {*
+  fun dest_cbinop t =
+    let
+      val (t2, rhs) = Thm.dest_comb t;
+      val (bop, lhs) = Thm.dest_comb t2;
+    in
+      (bop, (lhs, rhs))
+    end
+*}
 
-apply (tactic {* rtac man_inst 1 *})
 
-thm APPLY_RSP
+ML_prf {* val (a, b) = (snd (Thm.dest_abs NONE ct), (snd (Thm.dest_abs NONE goal'))) *}
+ML_prf {* val (a, b) = (snd (Thm.dest_abs NONE a), (snd (Thm.dest_abs NONE b))) *}
+ML_prf {* val (a, b) = (snd (Thm.dest_comb a), snd (Thm.dest_comb b)) *}
+ML_prf {* val (a, b) = ((fst o snd) (dest_cbinop a), (fst o snd) (dest_cbinop b)) *}
+ML_prf {* (term_of a, term_of b) *}
+ML_prf {* (Envir.beta_norm (term_of a), term_of b) *}
+ML_prf {* Thm.beta_conv *}
+ML_prf man_inst
+thm APPLY_RSP_I2
+apply (tactic {* compose_tac (false,man_inst,0) 1 *})
+
 sorry
 
 thm list.recs(2)