diff -r 1c43134ff988 -r 3803869014aa src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Fri Jul 01 15:14:44 2011 +0200
+++ b/src/Tools/Code/code_simp.ML	Fri Jul 01 15:16:03 2011 +0200
@@ -58,9 +58,10 @@
 
 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
 
-val setup = Method.setup (Binding.name "code_simp")
-  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
-  "simplification with code equations"
+val setup =
+  Method.setup @{binding code_simp}
+    (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
+    "simplification with code equations"
   #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);