--- a/QuotMain.thy	Wed Oct 21 10:55:32 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 11:50:53 2009 +0200
@@ -1350,14 +1350,27 @@
 ML_prf {*
   val goal = hd (prems_of (Isar.goal ()));
   val goalc = Logic.strip_assums_concl goal
-  val ps = rev (Logic.strip_params goal);
-  val (_, gc') = Thm.dest_comb (cterm_of @{theory} (Term.subst_bounds ((map Free ps), goalc)));
+  val ps = rev (map Free (Logic.strip_params goal));
+  val (_, gc') = Thm.dest_comb (cterm_of @{theory} (Term.subst_bounds (ps, goalc)));
   val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_II" }))
 *}
-
+ML_prf fold
 ML_prf {*
   val m = Thm.match (tc', gc')
+  val l = map (fst) (snd m);
+  val f_inst = map (term_of o snd) (snd m);
+  val f_abs = map (fold lambda ps) f_inst
 *}
+ML_prf {* val f_abs_c = map (cterm_of @{theory}) f_abs *}
+ML_prf {* val insts = l ~~ f_abs_c *}
+ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_II" } *}
+ML_prf {* Toplevel.program (fn () => cterm_instantiate insts t) *}
+
+ML_prf {* Toplevel.program (fn () => Drule.instantiate' [] [SOME f_abs_c, SOME f_abs_c] t) *}
+
+
+
+.
 (*  FAILS: t2 = Drule.instantiate m @{thm "APPLY_RSP_II" }; rtac t2 1 *)
 (* Works but why does it take a string? *)
 ML_prf {*