# HG changeset patch # User blanchet # Date 1307437972 -7200 # Node ID 3a8d49bc06e12249fbee9526c76d1417a8a20567 # Parent 9d717505595f24b20bb0fe0c4e4799ba23297c9a tuning diff -r 9d717505595f -r 3a8d49bc06e1 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Jun 07 11:05:09 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Jun 07 11:12:52 2011 +0200 @@ -243,7 +243,7 @@ o generic_metis_tac type_syss ctxt (schem_facts @ ths)) end -fun setup_method (binding, type_syss as type_sys :: _) = +fun setup_method (binding, type_syss) = (if type_syss = metis_default_type_syss then (Args.parens Parse.short_ident >> (fn s => AList.lookup (op =) type_sys_aliases s |> the_default s))