fixed type helper indices in new Metis

--- 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
@@ -127,7 +127,7 @@
   val translate_atp_fact :
     Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
     -> translated_formula option * ((string * locality) * thm)
-  val helper_table : (string * (bool * thm list)) list
+  val helper_table : ((string * bool) * thm list) list
   val should_specialize_helper : type_sys -> term -> bool
   val tfree_classes_of_terms : term list -> string list
   val tvar_classes_of_terms : term list -> string list
@@ -1253,42 +1253,38 @@
 
 (** Helper facts **)
 
-(* 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. *)
+(* The Boolean indicates that a fairly sound type encoding is needed. *)
 val helper_table =
-  [("COMBI", (false, @{thms Meson.COMBI_def})),
-   ("COMBK", (false, @{thms Meson.COMBK_def})),
-   ("COMBB", (false, @{thms Meson.COMBB_def})),
-   ("COMBC", (false, @{thms Meson.COMBC_def})),
-   ("COMBS", (false, @{thms Meson.COMBS_def})),
-   ("fequal",
+  [(("COMBI", false), @{thms Meson.COMBI_def}),
+   (("COMBK", false), @{thms Meson.COMBK_def}),
+   (("COMBB", false), @{thms Meson.COMBB_def}),
+   (("COMBC", false), @{thms Meson.COMBC_def}),
+   (("COMBS", false), @{thms Meson.COMBS_def}),
+   (("fequal", true),
     (* This is a lie: Higher-order equality doesn't need a sound type encoding.
        However, this is done so for backward compatibility: Including the
        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})),
-   ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
-   ("fTrue", (true, @{thms True_or_False})),
-   ("fNot",
-    (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
-                   fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
-   ("fconj",
-    (false,
-     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
-         by (unfold fconj_def) fast+})),
-   ("fdisj",
-    (false,
-     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
-         by (unfold fdisj_def) fast+})),
-   ("fimplies",
-    (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}))]
-  |> map (apsnd (apsnd (map zero_var_indexes)))
+    @{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}),
+   (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
+   (("fTrue", true), @{thms True_or_False}),
+   (("fNot", false),
+    @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+           fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
+   (("fconj", false),
+    @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
+        by (unfold fconj_def) fast+}),
+   (("fdisj", false),
+    @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
+        by (unfold fdisj_def) fast+}),
+   (("fimplies", 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})]
+  |> map (apsnd (map zero_var_indexes))
 
 val type_tag = `make_fixed_const type_tag_name
 
@@ -1331,7 +1327,7 @@
       val fairly_sound = is_type_sys_fairly_sound type_sys
     in
       helper_table
-      |> maps (fn (helper_s, (needs_fairly_sound, ths)) =>
+      |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
                   if helper_s <> unmangled_s orelse
                      (needs_fairly_sound andalso not fairly_sound) then
                     []

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -195,7 +195,7 @@
 fun generic_metis_tac modes type_sys ctxt ths i st0 =
   let
     val _ = trace_msg ctxt (fn () =>
-        "Metis called with theorems " ^
+        "Metis called with theorems\n" ^
         cat_lines (map (Display.string_of_thm ctxt) ths))
     fun tac clause = resolve_tac (FOL_SOLVE type_sys modes ctxt clause ths) 1
   in

--- 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
@@ -327,12 +327,14 @@
          String.isPrefix lightweight_tags_sym_formula_prefix ident then
         Isa_Reflexive_or_Trivial |> some
       else if String.isPrefix helper_prefix ident then
-        case space_explode "_" ident  of
-          _ :: const :: j :: _ =>
-          nth (helper_table |> filter (curry (op =) const o fst)
-                            |> maps (snd o snd))
+        case (String.isSuffix typed_helper_suffix ident,
+              space_explode "_" ident) of
+          (needs_fairly_sound, _ :: const :: j :: _) =>
+          nth ((const, needs_fairly_sound)
+               |> AList.lookup (op =) helper_table |> the)
               (the (Int.fromString j) - 1)
-          |> prepare_helper |> Isa_Raw |> some
+          |> prepare_helper
+          |> Isa_Raw |> some
         | _ => raise Fail ("malformed helper identifier " ^ quote ident)
       else case try (unprefix conjecture_prefix) ident of
         SOME s =>
@@ -424,8 +426,8 @@
           let
             val helper_ths =
               helper_table
-              |> filter (is_used o prefix const_prefix o fst)
-              |> maps (fn (_, (needs_full_types, thms)) =>
+              |> filter (is_used o prefix const_prefix o fst o fst)
+              |> maps (fn ((_, needs_full_types), thms) =>
                           if needs_full_types andalso mode <> FT then []
                           else map (`prepare_helper) thms)
           in problem |> fold (add_thm false) helper_ths end