--- a/src/HOL/Decision_Procs/langford.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Thu Aug 26 20:51:17 2010 +0200
@@ -185,7 +185,7 @@
| Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
| Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)