# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255773290 -7200
# Node ID 13575d73e435b99bc19cf1e5e9d33286908c0980
# Parent  28f7dbd99314366606365a176160c34df5fb37cd
compose_tac works with the full instantiation.

diff -r 28f7dbd99314 -r 13575d73e435 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 17 10:40:54 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 11:54:50 2009 +0200
@@ -1304,10 +1304,21 @@
 ML_prf {* val (a, b) = ((fst o snd) (dest_cbinop a), (fst o snd) (dest_cbinop b)) *}
 ML_prf {* (term_of a, term_of b) *}
 ML_prf {* (Envir.beta_norm (term_of a), term_of b) *}
-ML_prf {* Thm.beta_conv *}
-ML_prf man_inst
-thm APPLY_RSP_I2
-apply (tactic {* compose_tac (false,man_inst,0) 1 *})
+ML_prf {* val man_inst_norm_r = Drule.beta_eta_conversion (cprop_of man_inst) *}
+ML_prf {* val man_inst_norm = MetaSimplifier.rewrite_rule [man_inst_norm_r] man_inst *}
+ML_prf {*
+  val (tc') = (Logic.strip_assums_concl (prop_of man_inst_norm));
+  val ps = Logic.strip_params (prop_of man_inst_norm)
+  val tt = Term.list_abs (ps, tc')
+  val ct = cterm_of @{theory} tt
+*}
+ML_prf {* Thm.match (ct, goal') *}
+ML_prf {* PRIMSEQ *}
+ML_prf {* man_inst_norm *}
+apply (tactic {* compose_tac (false, man_inst_norm, 4) 1 *})
+
+
+
 
 sorry