diff -r 6f0d14ba096c -r 42a2cac76c41 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 20 19:46:22 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 10:30:29 2009 +0200
@@ -1228,9 +1228,11 @@
 ML {* val trm_r = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
+lemmas APPLY_RSP_II = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]
 
 ML {* val trm = build_goal_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
+
 prove list_induct_tr: trm_r
 apply (atomize(full))
 apply (simp only: id_def[symmetric])
@@ -1342,7 +1344,25 @@
 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 apply (rule QUOTIENT_fset)
 (* APPLY_RSP *)
-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"] )
+
+
+
+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 (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_II" }))
+*}
+
+ML_prf {*
+  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 *})
+(*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)
 apply (rule QUOTIENT_fset)
 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"])