| changeset 43329 | 84472e198515 |
| parent 35985 | 0bbf0d2348f9 |
| child 46497 | 89ccf66aa73d |
--- a/src/Pure/conjunction.ML Wed Jun 08 22:16:21 2011 +0200 +++ b/src/Pure/conjunction.ML Thu Jun 09 20:22:22 2011 +0200 @@ -130,7 +130,7 @@ local fun conjs thy n = - let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n) + let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invent Name.context "A" n) in (As, mk_conjunction_balanced As) end; val B = read_prop "B";