# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255766872 -7200
# Node ID 2c378008a7da00b59990d4165cb5d538921e7433
# Parent  22a503280debbab07e1495e90ca96693ef054bf5
Fully manually instantiated. Still fails...

diff -r 22a503280deb -r 2c378008a7da QuotMain.thy
--- a/QuotMain.thy	Sat Oct 17 09:04:24 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 10:07:52 2009 +0200
@@ -1264,34 +1264,25 @@
 ML_prf {* ct; goal'' *}
 
 ML_prf {* val nlct = cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I2" }) *}
+
 ML_prf {* Thm.match (nlct, goal'') *}
-ML_prf {* t *}
+ML_prf {* ct *}
 
 
 (*apply (tactic {*Cong_Tac.cong_tac @{thm APPLY_RSP_I2} 1 *}) *)
+ML_prf {* t *}
 ML_prf {*
-  Toplevel.program (fn () =>
-    Drule.instantiate' [] [NONE, SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). []"}] t
-  )
+  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). ([]::'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 pat = @{cpat "?f6 x y"}
-val arg = @{cterm "[]"}
-*}
-
-
-ML_prf {*
-  val m = Thm.match (pat, arg)
-*}
-
-ML_prf {*
-  val m = Thm.match (ct, goal')
-  val t2 = Drule.instantiate m @{thm "APPLY_RSP_I2" }
- *}
-apply (tactic {* rtac t2 1 *})
+apply (tactic {* rtac man_inst 1 *})
 
 thm APPLY_RSP
 sorry