# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255763064 -7200
# Node ID 22a503280debbab07e1495e90ca96693ef054bf5
# Parent  3cdb743b76059aa2d8fe7a673fa77348f974da7a
Little progress with match/instantiate

diff -r 3cdb743b7605 -r 22a503280deb QuotMain.thy
--- a/QuotMain.thy	Fri Oct 16 19:21:05 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 09:04:24 2009 +0200
@@ -1253,21 +1253,35 @@
   val goalc = Logic.strip_assums_concl goal
 *}
 ML_prf {*
-  val ps = Logic.strip_params goal
-  val goal' = cterm_of @{theory} (Term.list_abs (ps, goalc))
-*}
-ML_prf {* ct; goal' *}
-
-*)
-ML_prf {*
-val pat = @{cpat "\<lambda>x y. (?f6 x y (?x6 x y) = ?g6 x y (?y6 x y))"}
-val arg = @{cterm "\<lambda>x y. (x [] = y [])"}
+  val goalct = cterm_of @{theory} (hd ( prems_of (Isar.goal ())))
 *}
 
 ML_prf {*
-val pat = @{cpat "(?f6 x y (?x6) = ?g6 x y (?y6))"}
-val arg = @{cterm "(x [] = y [])"}
+  val ps = Logic.strip_params goal
+  val goal' = cterm_of @{theory} (Term.list_abs (ps, goalc))
+  val goal'' = cterm_of @{theory} (Term.subst_bounds ((map Free ps), goalc))
 *}
+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 *}
+
+
+(*apply (tactic {*Cong_Tac.cong_tac @{thm APPLY_RSP_I2} 1 *}) *)
+ML_prf {*
+  Toplevel.program (fn () =>
+    Drule.instantiate' [] [NONE, SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). []"}] t
+  )
+*}
+
+
+
+ML_prf {*
+val pat = @{cpat "?f6 x y"}
+val arg = @{cterm "[]"}
+*}
+
 
 ML_prf {*
   val m = Thm.match (pat, arg)