--- 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]})),
--- 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)