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.
compile
authorblanchet
Wed, 18 Apr 2012 10:53:28 +0200
changeset 47532 8e1a120ed492
parent 47531 7fe7c7419489
child 47533 5afe54e05406
compile
src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML file | annotate | diff | comparison | revisions
src/HOL/ex/sledgehammer_tactics.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle