--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 10:56:46 2010 +0200
@@ -777,7 +777,7 @@
$ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| (t0 as Const (@{const_name Ex}, _))
- $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
+ $ Abs (s', T', (t10 as @{const HOL.conj}) $ (t11 $ Bound 0) $ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| Const (@{const_name Let}, _) $ t1 $ t2 =>
do_term (betapply (t2, t1)) accum
@@ -883,8 +883,8 @@
| (t0 as Const (s0, _)) $ t1 $ t2 =>
if s0 = @{const_name "==>"} orelse
s0 = @{const_name Pure.conjunction} orelse
- s0 = @{const_name "op &"} orelse
- s0 = @{const_name "op |"} orelse
+ s0 = @{const_name HOL.conj} orelse
+ s0 = @{const_name HOL.disj} orelse
s0 = @{const_name HOL.implies} then
let
val impl = (s0 = @{const_name "==>"} orelse
@@ -975,7 +975,7 @@
do_all t0 s0 T1 t1 accum
| Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
consider_general_equals mdata true x t1 t2 accum
- | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
| (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
\do_formula", [t])