author | blanchet |
Wed, 20 Jul 2011 00:37:42 +0200 | |
changeset 43908 | e18c57d6225d |
parent 43907 | 073ab5379842 |
child 43909 | 7feb72f7bc3e |
--- a/src/HOL/Tools/Nitpick/nitrox.ML Wed Jul 20 00:37:42 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitrox.ML Wed Jul 20 00:37:42 2011 +0200 @@ -73,6 +73,7 @@ "$true" => @{const_name True} | "$false" => @{const_name False} | "=" => @{const_name HOL.eq} + | "equal" => @{const_name HOL.eq} | _ => x, map fastype_of ts ---> res_T) |> (if is_variable x then Free else Const), ts) end