Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Metis/metis_translate.ML
changeset 43175 4ca344fe0aca
parent 43174 f497a1e97d37
child 43180 283114859d6c 
--- 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)
isabelle