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