use right context for preplay, to avoid errors in fact lookup
authorblanchet
Mon, 22 Jun 2015 16:56:03 +0200
changeset 60548 e6adb8868478
parent 60547 a62655f925c8
child 60549 e168d5c48a95
use right context for preplay, to avoid errors in fact lookup
src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jun 22 16:56:03 2015 +0200
@@ -71,9 +71,11 @@
     (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
   else
     let
+      val ctxt = Proof.context_of state
+
+      val {facts = chained, goal, ...} = Proof.goal state
       val fact_names = map fst used_facts
 
-      val {context = ctxt, facts = chained, goal} = Proof.goal state
       val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
       val goal_t = Logic.list_implies (map Thm.prop_of chained @ hyp_ts, concl_t)