# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 4ca344fe0aca75525dce65d3d8610d0381d2c7d2
# Parent  f497a1e97d375b03f0f52d1210db6cf5acfe3b6f
properly locate helpers whose constants have several entries in the helper table

diff -r f497a1e97d37 -r 4ca344fe0aca src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -1266,7 +1266,9 @@
 
 (** Helper facts **)
 
-(* The Boolean indicates that a fairly sound type encoding is needed. *)
+(* The Boolean indicates that a fairly sound type encoding is needed.
+   "false" must precede "true" to ensure consistent numbering and a correct
+   mapping in Metis. *)
 val helper_table =
   [("COMBI", (false, @{thms Meson.COMBI_def})),
    ("COMBK", (false, @{thms Meson.COMBK_def})),
@@ -1279,10 +1281,10 @@
        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", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
    ("fFalse", (true, @{thms True_or_False})),
-   ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
+   ("fTrue", (false, [@{lemma "fTrue" by (unfold 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]
                    fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
diff -r f497a1e97d37 -r 4ca344fe0aca src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -329,7 +329,8 @@
       else if String.isPrefix helper_prefix ident then
         case space_explode "_" ident  of
           _ :: const :: j :: _ =>
-          nth (AList.lookup (op =) helper_table const |> the |> snd)
+          nth (helper_table |> filter (curry (op =) const o fst)
+                            |> maps (snd o snd))
               (the (Int.fromString j) - 1)
           |> prepare_helper |> Isa_Raw |> some
         | _ => raise Fail ("malformed helper identifier " ^ quote ident)