--- a/src/HOL/Tools/cnf_funcs.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Aug 26 20:51:17 2010 +0200
@@ -97,7 +97,7 @@
| is_atom (Const (@{const_name True}, _)) = false
| is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false
| is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
| is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
| is_atom (Const (@{const_name Not}, _) $ _) = false
| is_atom _ = true;
@@ -198,7 +198,7 @@
in
disj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy y
@@ -232,7 +232,7 @@
in
make_nnf_not_disj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.implies}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)