diff -r 2e9bf718a7a1 -r 65631ca437c9 src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOLP/simpdata.ML	Mon Dec 20 16:44:33 2010 +0100
@@ -17,15 +17,15 @@
 (* Conversion into rewrite rules *)
 
 fun mk_eq th = case concl_of th of
-      _ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
-    | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
+      _ $ (Const (@{const_name iff}, _) $ _ $ _) $ _ => th
+    | _ $ (Const (@{const_name eq}, _) $ _ $ _) $ _ => th
     | _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
     | _ => make_iff_T th;
 
 
 val mksimps_pairs =
-  [(@{const_name "op -->"}, [@{thm mp}]),
-   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+  [(@{const_name imp}, [@{thm mp}]),
+   (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
    (@{const_name "All"}, [@{thm spec}]),
    (@{const_name True}, []),
    (@{const_name False}, [])];