# HG changeset patch
# User haftmann
# Date 1276867564 -7200
# Node ID 7315100b916d88de28be49e5bc4965586ecad9ab
# Parent  802619d7576d51b0d68166681ec6372e7e057d47
code_simp: only succeed on real progress

diff -r 802619d7576d -r 7315100b916d src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Fri Jun 18 15:26:02 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Fri Jun 18 15:26:04 2010 +0200
@@ -75,7 +75,7 @@
 fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy;
 
 val setup = Method.setup (Binding.name "code_simp")
-  (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of))
+  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo current_tac o ProofContext.theory_of)))
   "simplification with code equations"
   #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);