| changeset 27333 | 7095f775131a |
| parent 27279 | 39ff18c0f07f |
| child 27865 | 27a8ad9612a3 |
--- a/src/Pure/drule.ML Mon Jun 23 23:45:45 2008 +0200 +++ b/src/Pure/drule.ML Mon Jun 23 23:45:46 2008 +0200 @@ -146,7 +146,7 @@ fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t; -val implies = certify Term.implies; +val implies = certify Logic.implies; fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B; (*cterm version of list_implies: [A1,...,An], B goes to [|A1;==>;An|]==>B *)