Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
code_simp: only succeed on real progress
authorhaftmann
Fri, 18 Jun 2010 15:26:04 +0200
changeset 37463 7315100b916d
parent 37462 802619d7576d
child 37464 9250ad1b98e0
code_simp: only succeed on real progress
src/Tools/Code/code_simp.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle