temporarily disable "fequal" handling in Metis;
one proof fails in "HOL-Auth" because of the new rules
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 20 15:16:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 20 15:56:00 2010 +0200
@@ -66,7 +66,7 @@
(* HOL to FOL (Isabelle to Metis) *)
(* ------------------------------------------------------------------------- *)
-fun fn_isa_to_met_sublevel "equal" = "c_fequal"
+fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
| fn_isa_to_met_sublevel x = x
fun fn_isa_to_met_toplevel "equal" = "="
| fn_isa_to_met_toplevel x = x