tuned -- with subtle change of order of evaluation;

--- 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