Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuning
authorblanchet
Tue, 07 Jun 2011 11:12:52 +0200
changeset 43235 3a8d49bc06e1
parent 43234 9d717505595f
child 43236 a1a0dcbeb785
tuning
src/HOL/Tools/Metis/metis_tactics.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle