diff -r 80ca4a065a48 -r 02924903a6fd src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/Doc/Codegen/Evaluation.thy	Sat Jul 18 20:54:56 2015 +0200
@@ -232,7 +232,7 @@
 ML_prf 
 (*>*) \<open>val thm =
   Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
-by (tactic \<open>ALLGOALS (rtac thm)\<close>)
+by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
 (*>*) 
 
 text \<open>