--- 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);