--- a/src/Tools/cong_tac.ML Thu Feb 20 18:23:32 2014 +0100
+++ b/src/Tools/cong_tac.ML Thu Feb 20 19:32:20 2014 +0100
@@ -21,14 +21,15 @@
_ $ (_ $ (f $ x) $ (g $ y)) =>
let
val cong' = Thm.lift_rule cgoal cong;
- val _ $ (_ $ (f' $ x') $ (g' $ y')) =
- Logic.strip_assums_concl (Thm.prop_of cong');
+ val _ $ (_ $ (f' $ x') $ (g' $ y')) = 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)]
+ val insts =
+ [(f', f), (g', g), (x', x), (y', y)]
|> 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
+ fn st =>
+ compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
+ handle THM _ => no_tac st
end
| _ => no_tac)
end);