# HG changeset patch
# User blanchet
# Date 1292599202 -3600
# Node ID 15ba335d0ba2f7c56aa870e4325f44e9fdade16b
# Parent  8edeb1dbbc767b91d8e9e63f2b313dc69ec70222
compile

diff -r 8edeb1dbbc76 -r 15ba335d0ba2 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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
diff -r 8edeb1dbbc76 -r 15ba335d0ba2 src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML
--- 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