tuning
authorblanchet
Mon, 25 Jul 2011 14:10:12 +0200
changeset 43963 78c723cc3d99
parent 43962 e1d29c3ca933
child 43964 9338aa218f09
tuning
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