--- a/src/Tools/cong_tac.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Tools/cong_tac.ML Sat Jan 14 21:16:15 2012 +0100
@@ -25,7 +25,7 @@
Logic.strip_assums_concl (Thm.prop_of cong');
val ps = Logic.strip_params (Thm.concl_of cong');
val insts = [(f', f), (g', g), (x', x), (y', y)]
- |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
+ |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
in
fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
handle THM _ => no_tac st