# HG changeset patch
# User blanchet
# Date 1334739208 -7200
# Node ID 8e1a120ed492503dc9e1a2eb26eec283eec3df5e
# Parent  7fe7c741948927643e72de7d90513e7750d32b9e
compile

diff -r 7fe7c7419489 -r 8e1a120ed492 src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML	Wed Apr 18 10:53:28 2012 +0200
+++ b/src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML	Wed Apr 18 10:53:28 2012 +0200
@@ -475,8 +475,7 @@
         val problem =
           {state = st', goal = goal, subgoal = i,
            subgoal_count = Sledgehammer_Util.subgoal_count st,
-           facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
-           smt_filter = NONE}
+           facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
       in prover params (K (K (K ""))) problem end)) ()
       handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate
diff -r 7fe7c7419489 -r 8e1a120ed492 src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Wed Apr 18 10:53:28 2012 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Wed Apr 18 10:53:28 2012 +0200
@@ -46,8 +46,7 @@
              relevance_fudge relevance_override chained_ths hyp_ts concl_t
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       facts = map Sledgehammer_Provers.Untranslated_Fact facts,
-       smt_filter = NONE}
+       facts = map Sledgehammer_Provers.Untranslated_Fact facts}
   in
     (case prover params (K (K (K ""))) problem of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME