1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 22 18:47:45 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 22 19:08:25 2010 +0200
     1.3 @@ -299,6 +299,7 @@
     1.4  
     1.5  fun run_sh prover hard_timeout timeout dir st =
     1.6    let
     1.7 +    val _ = Sledgehammer_Fact_Filter.use_natural_form := true (* experimental *)
     1.8      val {context = ctxt, facts, goal} = Proof.goal st
     1.9      val thy = ProofContext.theory_of ctxt
    1.10      val change_dir = (fn SOME d => Config.put ATP_Systems.dest_dir d | _ => I)
    1.11 @@ -324,7 +325,7 @@
    1.12        NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
    1.13      | SOME _ => (message, SH_FAIL (time_isa, time_atp))
    1.14    end
    1.15 -  handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, []))
    1.16 +  handle Sledgehammer_HOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
    1.17         | ERROR msg => ("error: " ^ msg, SH_ERROR)
    1.18         | TimeLimit.TimeOut => ("timeout", SH_ERROR)
    1.19