src/HOL/Library/Eval_Witness.thy

--- a/src/HOL/Library/Eval_Witness.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -84,7 +84,7 @@
 
 in
   Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
-    Method.SIMPLE_METHOD' (eval_tac ws))
+    SIMPLE_METHOD' (eval_tac ws))
 end
 *} "Evaluation with ML witnesses"