src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 38786 e46e7a9cb622
parent 38652 e063be321438
child 38795 848be46708dc
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -411,7 +411,7 @@
     1.4     (@{const_name "op ="}, 1),
     1.5     (@{const_name "op &"}, 2),
     1.6     (@{const_name "op |"}, 2),
     1.7 -   (@{const_name "op -->"}, 2),
     1.8 +   (@{const_name HOL.implies}, 2),
     1.9     (@{const_name If}, 3),
    1.10     (@{const_name Let}, 2),
    1.11     (@{const_name Pair}, 2),
    1.12 @@ -1454,7 +1454,7 @@
    1.13    | @{const Trueprop} $ t1 => lhs_of_equation t1
    1.14    | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
    1.15    | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
    1.16 -  | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
    1.17 +  | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
    1.18    | _ => NONE
    1.19  fun is_constr_pattern _ (Bound _) = true
    1.20    | is_constr_pattern _ (Var _) = true