1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jul 25 14:10:12 2011 +0200
     1.3 @@ -249,9 +249,7 @@
     1.4  
     1.5  fun setup_method (binding, type_syss) =
     1.6    ((Args.parens (Scan.repeat Parse.short_ident)
     1.7 -    >> maps (fn s => case AList.lookup (op =) type_enc_aliases s of
     1.8 -                       SOME tss => tss
     1.9 -                     | NONE => [s]))
    1.10 +    >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
    1.11      |> Scan.option |> Scan.lift)
    1.12    -- Attrib.thms >> (METHOD oo method type_syss)
    1.13    |> Method.setup binding