--- a/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 10:56:46 2010 +0200
@@ -1952,9 +1952,9 @@
| NONE => error "num_of_term: unsupported dvd")
| fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
@{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (@{term "op &"} $ t1 $ t2) =
+ | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) =
@{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
+ | fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) =
@{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
@@ -2016,7 +2016,7 @@
fun term_bools acc t =
let
- val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
+ val is_op = member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
@{term "op = :: int => _"}, @{term "op < :: int => _"},
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
@{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]