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])