# HG changeset patch
# User wenzelm
# Date 1214257546 -7200
# Node ID 7095f775131af7ce6801b245f35427cf70045661
# Parent  94790a9620c3cb079fbbec026d6da8acdca8ba64
Logic.implies;

diff -r 94790a9620c3 -r 7095f775131a src/Pure/drule.ML
--- 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 *)