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/HOL/Tools/function_package/fundef_package.ML
changeset 24977 9f98751c9628
parent 24867 e5b55d7be9bb
child 25045 12386aefe9ac 
--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 11 19:10:17 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 11 19:10:19 2007 +0200
@@ -202,7 +202,7 @@
 
       val t' = new_subg
                 |> fold forall_elim cps
-                |> flip implies_elim (fold forall_elim cps sg2)
+                |> Thm.elim_implies (fold forall_elim cps sg2)
                 |> fold_rev forall_intr cps
 
       val st' = implies_elim st t'
isabelle