Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/cong_tac.ML
changeset 60784 4f590c08fd5d
parent 59642 929984c529d3 
--- a/src/Tools/cong_tac.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/Tools/cong_tac.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -23,11 +23,11 @@
           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)]
-            |> map (fn (t, u) => apply2 (Thm.cterm_of ctxt) (Term.head_of t, fold_rev Term.abs ps u));
+            [(f', f), (g', g), (x', x), (y', y)] |> map (fn (t, u) =>
+              (#1 (dest_Var (head_of t)), Thm.cterm_of ctxt (fold_rev Term.abs ps u)));
         in
           fn st =>
-            compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
+            compose_tac ctxt (false, infer_instantiate ctxt insts cong', 2) i st
               handle THM _ => no_tac st
         end
     | _ => no_tac)
isabelle