# HG changeset patch
# User blanchet
# Date 1407406661 -7200
# Node ID 7a9aaddb3203c59a2fdc9b1ed4b8a0d881f78866
# Parent  0a84dc31601fb17f73c556b53d9386e1a627d9f6
compile

diff -r 0a84dc31601f -r 7a9aaddb3203 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -534,7 +534,7 @@
           timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
         fun sledge_tac time_slice prover type_enc =
           Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-            (override_params prover type_enc (my_timeout time_slice)) fact_override
+            (override_params prover type_enc (my_timeout time_slice)) fact_override []
       in
         if !meth = "sledgehammer_tac" then
           sledge_tac 0.2 ATP_Proof.vampireN "mono_native"