# HG changeset patch
# User blanchet
# Date 1305888478 -7200
# Node ID 221af561ebf9c23cab531a537ada5bec90f30ccb
# Parent  3b9669b11d33d30543f6f4d106259cb33c1fda3b
tuning

diff -r 3b9669b11d33 -r 221af561ebf9 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Fri May 20 12:47:58 2011 +0200
@@ -654,11 +654,9 @@
        equality helpers by default in Metis breaks a few existing proofs. *)
     (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
                   fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
-   ("fFalse", (true, [@{lemma "x = fTrue | x = fFalse"
-                          by (unfold fFalse_def fTrue_def) fast}])),
+   ("fFalse", (true, @{thms True_or_False})),
    ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
-   ("fTrue", (true, [@{lemma "x = fTrue | x = fFalse"
-                         by (unfold fFalse_def fTrue_def) fast}])),
+   ("fTrue", (true, @{thms True_or_False})),
    ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
    ("fNot",
     (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
@@ -673,7 +671,7 @@
     (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
                     "~ fimplies P Q | ~ P | Q"
               by (unfold fimplies_def) fast+})),
-   ("If", (true, @{thms if_True if_False True_or_False})) (* FIXME *)]
+   ("If", (true, @{thms if_True if_False True_or_False}))]
 
 (* ------------------------------------------------------------------------- *)
 (* Logic maps manage the interface between HOL and first-order logic.        *)