# HG changeset patch
# User blanchet
# Date 1277226505 -7200
# Node ID de91b800c34e98021fd691091f6762f079d3148c
# Parent  32a1ee39c49b2dc6e59853ba1e35084112b7c7de
turn on "natural form" filtering in the Mirabelle tests, to see how it performs

diff -r 32a1ee39c49b -r de91b800c34e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 22 18:47:45 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 22 19:08:25 2010 +0200
@@ -299,6 +299,7 @@
 
 fun run_sh prover hard_timeout timeout dir st =
   let
+    val _ = Sledgehammer_Fact_Filter.use_natural_form := true (* experimental *)
     val {context = ctxt, facts, goal} = Proof.goal st
     val thy = ProofContext.theory_of ctxt
     val change_dir = (fn SOME d => Config.put ATP_Systems.dest_dir d | _ => I)
@@ -324,7 +325,7 @@
       NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
     | SOME _ => (message, SH_FAIL (time_isa, time_atp))
   end
-  handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, []))
+  handle Sledgehammer_HOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
        | ERROR msg => ("error: " ^ msg, SH_ERROR)
        | TimeLimit.TimeOut => ("timeout", SH_ERROR)