src/HOL/Tools/Metis/metis_translate.ML

          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 (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)
       else case try (unprefix conjecture_prefix) ident of
         SOME s =>