src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 38786 e46e7a9cb622
parent 38199 8a9cace789d6
child 38795 848be46708dc
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -774,7 +774,7 @@
     1.4                          (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
     1.5                        end))
     1.6           | (t0 as Const (@{const_name All}, _))
     1.7 -           $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
     1.8 +           $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
     1.9             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
    1.10           | (t0 as Const (@{const_name Ex}, _))
    1.11             $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
    1.12 @@ -885,10 +885,10 @@
    1.13                  s0 = @{const_name Pure.conjunction} orelse
    1.14                  s0 = @{const_name "op &"} orelse
    1.15                  s0 = @{const_name "op |"} orelse
    1.16 -                s0 = @{const_name "op -->"} then
    1.17 +                s0 = @{const_name HOL.implies} then
    1.18                 let
    1.19                   val impl = (s0 = @{const_name "==>"} orelse
    1.20 -                             s0 = @{const_name "op -->"})
    1.21 +                             s0 = @{const_name HOL.implies})
    1.22                   val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
    1.23                   val (m2, accum) = do_formula sn t2 accum
    1.24                 in
    1.25 @@ -976,7 +976,7 @@
    1.26            | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
    1.27              consider_general_equals mdata true x t1 t2 accum
    1.28            | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
    1.29 -          | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
    1.30 +          | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
    1.31            | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
    1.32                               \do_formula", [t])
    1.33      in do_formula t end