# HG changeset patch
# User wenzelm
# Date 1465379623 -7200
# Node ID 94d1f820130fb29c684b5d5bcf798ae7b393930c
# Parent  74a4299632ae48f379e14da3a2c9998ee94ccd88
provide dynamic facts in static context, to allow use of method_facts during static closure;

diff -r 74a4299632ae -r 94d1f820130f src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Jun 08 11:33:56 2016 +0200
+++ b/src/Pure/Isar/method.ML	Wed Jun 08 11:53:43 2016 +0200
@@ -565,15 +565,14 @@
 
 in
 
-fun evaluate text static_ctxt =
+fun evaluate text ctxt0 facts =
   let
-    fun eval0 m =
-      Seq.single #> Seq.maps_results (fn (ctxt, st) => m (get_facts ctxt) (ctxt, st));
-    fun eval (Basic m) = eval0 (m static_ctxt)
-      | eval (Source src) = eval0 (method_cmd static_ctxt src static_ctxt)
+    val ctxt = set_facts facts ctxt0;
+    fun eval0 m = Seq.single #> Seq.maps_results (m facts);
+    fun eval (Basic m) = eval0 (m ctxt)
+      | eval (Source src) = eval0 (method_cmd ctxt src ctxt)
       | eval (Combinator (_, c, txts)) = combinator c (map eval txts);
-    val method = eval text;
-  in fn facts => fn (ctxt, st) => method (Seq.Result (set_facts facts ctxt, st)) end;
+  in eval text o Seq.Result end;
 
 end;