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
```