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/Pure/variable.ML
changeset 46497 89ccf66aa73d
parent 45666 d83797ef0d2d
child 46869 26a9a4e0a631 
--- a/src/Pure/variable.ML	Wed Feb 15 22:44:31 2012 +0100
+++ b/src/Pure/variable.ML	Wed Feb 15 23:19:30 2012 +0100
@@ -539,7 +539,7 @@
   in (((xs ~~ ps), t'), ctxt') end;
 
 fun forall_elim_prop t prop =
-  Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
+  Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t)
   |> Thm.cprop_of |> Thm.dest_arg;
 
 fun focus_cterm goal ctxt =
isabelle