--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 20:51:17 2010 +0200
@@ -69,7 +69,7 @@
Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
| negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
- | negate_term (@{const "op -->"} $ t1 $ t2) =
+ | negate_term (@{const HOL.implies} $ t1 $ t2) =
@{const "op &"} $ t1 $ negate_term t2
| negate_term (@{const "op &"} $ t1 $ t2) =
@{const "op |"} $ negate_term t1 $ negate_term t2