src/HOL/HOL.thy

 method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
   "solve goal by evaluation"
 
 method_setup normalization = {*
   Scan.succeed (K (SIMPLE_METHOD'
-    (CHANGED_PROP o CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))
+    (CHANGED_PROP o (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k))))))
 *} "solve goal by normalization"
 
 
 subsection {* Counterexample Search Units *}