1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -1266,7 +1266,9 @@
     1.4  
     1.5  (** Helper facts **)
     1.6  
     1.7 -(* The Boolean indicates that a fairly sound type encoding is needed. *)
     1.8 +(* The Boolean indicates that a fairly sound type encoding is needed.
     1.9 +   "false" must precede "true" to ensure consistent numbering and a correct
    1.10 +   mapping in Metis. *)
    1.11  val helper_table =
    1.12    [("COMBI", (false, @{thms Meson.COMBI_def})),
    1.13     ("COMBK", (false, @{thms Meson.COMBK_def})),
    1.14 @@ -1279,10 +1281,10 @@
    1.15         equality helpers by default in Metis breaks a few existing proofs. *)
    1.16      (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.17                    fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    1.18 +   ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
    1.19     ("fFalse", (true, @{thms True_or_False})),
    1.20 -   ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
    1.21 +   ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
    1.22     ("fTrue", (true, @{thms True_or_False})),
    1.23 -   ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
    1.24     ("fNot",
    1.25      (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.26                     fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),

     2.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     2.3 @@ -329,7 +329,8 @@
     2.4        else if String.isPrefix helper_prefix ident then
     2.5          case space_explode "_" ident  of
     2.6            _ :: const :: j :: _ =>
     2.7 -          nth (AList.lookup (op =) helper_table const |> the |> snd)
     2.8 +          nth (helper_table |> filter (curry (op =) const o fst)
     2.9 +                            |> maps (snd o snd))
    2.10                (the (Int.fromString j) - 1)
    2.11            |> prepare_helper |> Isa_Raw |> some
    2.12          | _ => raise Fail ("malformed helper identifier " ^ quote ident)