1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -329,7 +329,8 @@
     1.4        else if String.isPrefix helper_prefix ident then
     1.5          case space_explode "_" ident  of
     1.6            _ :: const :: j :: _ =>
     1.7 -          nth (AList.lookup (op =) helper_table const |> the |> snd)
     1.8 +          nth (helper_table |> filter (curry (op =) const o fst)
     1.9 +                            |> maps (snd o snd))
    1.10                (the (Int.fromString j) - 1)
    1.11            |> prepare_helper |> Isa_Raw |> some
    1.12          | _ => raise Fail ("malformed helper identifier " ^ quote ident)