--- a/src/HOL/Tools/refute.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/refute.ML Fri Aug 27 10:56:46 2010 +0200
@@ -648,8 +648,8 @@
| Const (@{const_name All}, _) => t
| Const (@{const_name Ex}, _) => t
| Const (@{const_name "op ="}, _) => t
- | Const (@{const_name "op &"}, _) => t
- | Const (@{const_name "op |"}, _) => t
+ | Const (@{const_name HOL.conj}, _) => t
+ | Const (@{const_name HOL.disj}, _) => t
| Const (@{const_name HOL.implies}, _) => t
(* sets *)
| Const (@{const_name Collect}, _) => t
@@ -824,8 +824,8 @@
| Const (@{const_name All}, T) => collect_type_axioms T axs
| Const (@{const_name Ex}, T) => collect_type_axioms T axs
| Const (@{const_name "op ="}, T) => collect_type_axioms T axs
- | Const (@{const_name "op &"}, _) => axs
- | Const (@{const_name "op |"}, _) => axs
+ | Const (@{const_name HOL.conj}, _) => axs
+ | Const (@{const_name HOL.disj}, _) => axs
| Const (@{const_name HOL.implies}, _) => axs
(* sets *)
| Const (@{const_name Collect}, T) => collect_type_axioms T axs
@@ -1861,7 +1861,7 @@
SOME (interpret thy model args (eta_expand t 1))
| Const (@{const_name "op ="}, _) =>
SOME (interpret thy model args (eta_expand t 2))
- | Const (@{const_name "op &"}, _) $ t1 $ t2 =>
+ | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret thy model args t1
@@ -1871,14 +1871,14 @@
in
SOME (Leaf [fmTrue, fmFalse], m2, a2)
end
- | Const (@{const_name "op &"}, _) $ t1 =>
+ | Const (@{const_name HOL.conj}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op &"}, _) =>
+ | Const (@{const_name HOL.conj}, _) =>
SOME (interpret thy model args (eta_expand t 2))
(* this would make "undef" propagate, even for formulae like *)
(* "False & undef": *)
(* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
- | Const (@{const_name "op |"}, _) $ t1 $ t2 =>
+ | Const (@{const_name HOL.disj}, _) $ t1 $ t2 =>
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret thy model args t1
@@ -1888,9 +1888,9 @@
in
SOME (Leaf [fmTrue, fmFalse], m2, a2)
end
- | Const (@{const_name "op |"}, _) $ t1 =>
+ | Const (@{const_name HOL.disj}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op |"}, _) =>
+ | Const (@{const_name HOL.disj}, _) =>
SOME (interpret thy model args (eta_expand t 2))
(* this would make "undef" propagate, even for formulae like *)
(* "True | undef": *)