src/HOL/Eisbach/Eisbach.thy

--- a/src/HOL/Eisbach/Eisbach.thy	Mon Aug 12 21:22:40 2019 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy	Tue Aug 13 10:27:21 2019 +0200
@@ -41,7 +41,7 @@
      (Seq.make_results (Seq.single (ctxt', thm)))))\<close>
 
 ML \<open>fun method_evaluate text ctxt facts =
-  Method.NO_CONTEXT_TACTIC ctxt
+  NO_CONTEXT_TACTIC ctxt
     (Method.evaluate_runtime text ctxt facts)\<close>
 
 method_setup timeit =