diff -r 42a2cac76c41 -r efb427ae04c9 QuotMain.thy
--- a/QuotMain.thy	Wed Oct 21 10:30:29 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 10:55:32 2009 +0200
@@ -1359,8 +1359,15 @@
   val m = Thm.match (tc', gc')
 *}
 (*  FAILS: t2 = Drule.instantiate m @{thm "APPLY_RSP_II" }; rtac t2 1 *)
-(* Works but why does it take a string? *}
-apply (tactic {* res_inst_tac @{context} [(("f",0),"\<lambda>x. h # x"),(("g",0),"\<lambda>x. h # x")] @{thm "APPLY_RSP_II" } 1 *})
+(* Works but why does it take a string? *)
+ML_prf {*
+  val t_inst = snd m;
+  val t_insts = map (fn (a, b) => (fst (dest_Var (term_of a)), (Syntax.string_of_term @{context} (term_of b)))) t_inst
+  
+*}
+ML_prf dest_Var
+apply (tactic {* res_inst_tac @{context} [(("f",0),"op # h"),(("g",0),"op # h")] @{thm "APPLY_RSP_II" } 1 *})
+ML_prf induct_tac
 (*apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] )*)
 
 apply (rule QUOTIENT_fset)