--- 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)