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/Boogie/Tools/boogie_vcs.ML
changeset 46497 89ccf66aa73d
parent 41620 f88eca2e9ebd 
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Wed Feb 15 23:19:30 2012 +0100
@@ -220,7 +220,7 @@
 
 fun join (Assume (_, pv), pthm) (Assume (t, v), thm) =
       let
-        val mk_prop = Thm.capply @{cterm Trueprop}
+        val mk_prop = Thm.apply @{cterm Trueprop}
         val ct = Thm.cprop_of thm |> Thm.dest_arg |> Thm.dest_arg1 |> mk_prop
         val th = Thm.assume ct
         val (v', thm') = join (pv, imp_elim th pthm) (v, imp_elim th thm)
isabelle