parse equalities correctly in Nitrox parser
authorblanchet
Wed, 20 Jul 2011 00:37:42 +0200
changeset 43908 e18c57d6225d
parent 43907 073ab5379842
child 43909 7feb72f7bc3e
parse equalities correctly in Nitrox parser
src/HOL/Tools/Nitpick/nitrox.ML
--- 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