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