Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 42642 f5b4b9d4acda
parent 42638 a7a30721767a
child 42725 64dea91bbe0e 
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 02 22:52:15 2011 +0200
@@ -362,7 +362,7 @@
       st |> Proof.map_context
                 (change_dir dir
                  #> Config.put Sledgehammer_Provers.measure_run_time true)
-    val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
+    val params as {relevance_thresholds, max_relevant, slicing, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
            ("type_sys", type_sys),
isabelle