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