# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID b817c6f91a98e7c66ad70ed87425f06e1c70ee74
# Parent  59753d5448e0b68964dff75fd3fd64c2657710d9
reenabled equality proxy in Metis for higher-order reasoning

diff -r 59753d5448e0 -r b817c6f91a98 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -532,7 +532,7 @@
   | string_of_mode HO = "HO"
   | string_of_mode FT = "FT"
 
-fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
+fun fn_isa_to_met_sublevel "equal" = "c_fequal"
   | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
   | fn_isa_to_met_sublevel "c_True" = "c_fTrue"
   | fn_isa_to_met_sublevel "c_Not" = "c_fNot"