# HG changeset patch
# User wenzelm
# Date 1450790619 -3600
# Node ID d5ddd4866b7b46227116b2ef587b60a625386011
# Parent  4d162c237e4819f2c5fc41650354e8334c94dee7
tuned -- with subtle change of order of evaluation;

diff -r 4d162c237e48 -r d5ddd4866b7b src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 14:20:17 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 14:23:39 2015 +0100
@@ -147,17 +147,17 @@
   in (named_thm, parser) end;
 
 
-fun method_evaluate text ctxt facts =
+fun method_evaluate text ctxt =
   let
-    val eval_named_theorems =
-      (Method.map_source o map o Token.map_facts)
+    val text' =
+      text |> (Method.map_source o map o Token.map_facts)
         (fn SOME name =>
               (case Proof_Context.lookup_fact ctxt name of
                 SOME (false, ths) => K ths
               | _ => I)
           | NONE => I);
     val ctxt' = Config.put Method.closure false ctxt;
-  in Method.RUNTIME (fn st => Method.evaluate (eval_named_theorems text) ctxt' facts st) end;
+  in fn facts => Method.RUNTIME (fn st => Method.evaluate text' ctxt' facts st) end;
 
 fun method_instantiate env text =
   let