# HG changeset patch
# User boehmes
# Date 1288107354 -7200
# Node ID 2963511e121c576324e90da62bb103c9e13fe1d6
# Parent  8d470bbaafd791a6e90103c7b7e686d2e2e0396f
use proper context

diff -r 8d470bbaafd7 -r 2963511e121c src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 17:35:52 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 17:35:54 2010 +0200
@@ -423,9 +423,9 @@
 
 fun smt_filter run_remote time_limit st xrules i =
   let
-    val {context, facts, goal} = Proof.goal st
+    val {facts, goal, ...} = Proof.goal st
     val ctxt =
-      context
+      Proof.context_of st
       |> Config.put timeout (Time.toSeconds time_limit)
       |> Config.put oracle false
       |> Config.put filter_only true