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
Fri, 17 Dec 2010 16:20:02 +0100
changeset 41243 15ba335d0ba2
parent 41242 8edeb1dbbc76
child 41244 7c05c8301d7e
compile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML file | annotate | diff | comparison | revisions
src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Dec 17 15:30:43 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Dec 17 16:20:02 2010 +0100
@@ -376,7 +376,8 @@
     val problem =
       {state = st', goal = goal, subgoal = i,
        subgoal_count = Sledgehammer_Util.subgoal_count st,
-       facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
+       facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
+       smt_head = NONE}
     val time_limit =
       (case hard_timeout of
         NONE => I
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Fri Dec 17 15:30:43 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Fri Dec 17 16:20:02 2010 +0100
@@ -47,7 +47,8 @@
                         (prop_of goal))
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       facts = map Sledgehammer_Provers.Untranslated_Fact facts}
+       facts = map Sledgehammer_Provers.Untranslated_Fact facts,
+       smt_head = NONE}
   in
     (case prover params (K "") problem of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
isabelle