# HG changeset patch
# User blanchet
# Date 1311595812 -7200
# Node ID 78c723cc3d99bd0bc1da7230e47d1e465b6f07b2
# Parent  e1d29c3ca9334be3e2bfa75d66692ffbf540748e
tuning

diff -r e1d29c3ca933 -r 78c723cc3d99 src/HOL/Tools/Metis/metis_tactics.ML
--- 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