src/HOL/Tools/Metis/metis_translate.ML
changeset 43194 ef3ff8856245
parent 43193 e11bd628f1a5
child 43199 45f33d290615
     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 @@ -327,12 +327,14 @@
     1.4           String.isPrefix lightweight_tags_sym_formula_prefix ident then
     1.5          Isa_Reflexive_or_Trivial |> some
     1.6        else if String.isPrefix helper_prefix ident then
     1.7 -        case space_explode "_" ident  of
     1.8 -          _ :: const :: j :: _ =>
     1.9 -          nth (helper_table |> filter (curry (op =) const o fst)
    1.10 -                            |> maps (snd o snd))
    1.11 +        case (String.isSuffix typed_helper_suffix ident,
    1.12 +              space_explode "_" ident) of
    1.13 +          (needs_fairly_sound, _ :: const :: j :: _) =>
    1.14 +          nth ((const, needs_fairly_sound)
    1.15 +               |> AList.lookup (op =) helper_table |> the)
    1.16                (the (Int.fromString j) - 1)
    1.17 -          |> prepare_helper |> Isa_Raw |> some
    1.18 +          |> prepare_helper
    1.19 +          |> Isa_Raw |> some
    1.20          | _ => raise Fail ("malformed helper identifier " ^ quote ident)
    1.21        else case try (unprefix conjecture_prefix) ident of
    1.22          SOME s =>
    1.23 @@ -424,8 +426,8 @@
    1.24            let
    1.25              val helper_ths =
    1.26                helper_table
    1.27 -              |> filter (is_used o prefix const_prefix o fst)
    1.28 -              |> maps (fn (_, (needs_full_types, thms)) =>
    1.29 +              |> filter (is_used o prefix const_prefix o fst o fst)
    1.30 +              |> maps (fn ((_, needs_full_types), thms) =>
    1.31                            if needs_full_types andalso mode <> FT then []
    1.32                            else map (`prepare_helper) thms)
    1.33            in problem |> fold (add_thm false) helper_ths end