| changeset 46497 | 89ccf66aa73d |
| parent 43329 | 84472e198515 |
| child 56436 | 30ccec1e82fb |
--- a/src/Pure/conjunction.ML Wed Feb 15 22:44:31 2012 +0100 +++ b/src/Pure/conjunction.ML Wed Feb 15 23:19:30 2012 +0100 @@ -35,7 +35,7 @@ val true_prop = certify Logic.true_prop; val conjunction = certify Logic.conjunction; -fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B; +fun mk_conjunction (A, B) = Thm.apply (Thm.apply conjunction A) B; fun mk_conjunction_balanced [] = true_prop | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;