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.
made SML/NJ happy again;
authorwenzelm
Mon, 07 Jun 2010 17:13:36 +0200
changeset 37359 7b0ccc20cddc
parent 37358 74fb4f03bb51
child 37360 a2cde14de400
child 37361 250f487b3034
child 37383 22757d15cd86
made SML/NJ happy again;
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jun 07 16:00:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jun 07 17:13:36 2010 +0200
@@ -261,7 +261,7 @@
   end
 
 fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
-                     (relevance_override as {add, del, ...}) ctab =
+                     (relevance_override as {add, del, only}) ctab =
   let
     val thy = ProofContext.theory_of ctxt
     val add_thms = cnf_for_facts ctxt add
isabelle