src/HOL/Tools/Nitpick/nitpick_mono.ML
 changeset 38795 848be46708dc parent 38786 e46e7a9cb622 child 38864 4abe644fcea5
1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Aug 27 10:55:20 2010 +0200
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Aug 27 10:56:46 2010 +0200
1.3 @@ -777,7 +777,7 @@
1.4             \$ Abs (s', T', (t10 as @{const HOL.implies}) \$ (t11 \$ Bound 0) \$ t12) =>
1.5             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
1.6           | (t0 as Const (@{const_name Ex}, _))
1.7 -           \$ Abs (s', T', (t10 as @{const "op &"}) \$ (t11 \$ Bound 0) \$ t12) =>
1.8 +           \$ Abs (s', T', (t10 as @{const HOL.conj}) \$ (t11 \$ Bound 0) \$ t12) =>
1.9             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
1.10           | Const (@{const_name Let}, _) \$ t1 \$ t2 =>
1.11             do_term (betapply (t2, t1)) accum
1.12 @@ -883,8 +883,8 @@
1.13             | (t0 as Const (s0, _)) \$ t1 \$ t2 =>
1.14               if s0 = @{const_name "==>"} orelse
1.15                  s0 = @{const_name Pure.conjunction} orelse
1.16 -                s0 = @{const_name "op &"} orelse
1.17 -                s0 = @{const_name "op |"} orelse
1.18 +                s0 = @{const_name HOL.conj} orelse
1.19 +                s0 = @{const_name HOL.disj} orelse
1.20                  s0 = @{const_name HOL.implies} then
1.21                 let
1.22                   val impl = (s0 = @{const_name "==>"} orelse
1.23 @@ -975,7 +975,7 @@
1.24              do_all t0 s0 T1 t1 accum
1.25            | Const (x as (@{const_name "op ="}, _)) \$ t1 \$ t2 =>
1.26              consider_general_equals mdata true x t1 t2 accum
1.27 -          | (t0 as @{const "op &"}) \$ t1 \$ t2 => do_conjunction t0 t1 t2 accum
1.28 +          | (t0 as @{const HOL.conj}) \$ t1 \$ t2 => do_conjunction t0 t1 t2 accum
1.29            | (t0 as @{const HOL.implies}) \$ t1 \$ t2 => do_implies t0 t1 t2 accum
1.30            | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
1.31                               \do_formula", [t])