# HG changeset patch
# User blanchet
# Date 1434984963 -7200
# Node ID e6adb8868478f023755c2dfc4d61ef82e332d2df
# Parent  a62655f925c85fd31c14d36aa9043c8c14e2c296
use right context for preplay, to avoid errors in fact lookup

diff -r a62655f925c8 -r e6adb8868478 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)