# HG changeset patch
# User haftmann
# Date 1283409625 -7200
# Node ID 7cf8beb31e0fb1ab67fe6ee3e7ad3221cbacb6e5
# Parent  4bf80c23320e5c32e7a22960cf656ba4cf87ded0
normalization fails on unchanged goal

diff -r 4bf80c23320e -r 7cf8beb31e0f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 01 23:03:31 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 02 08:40:25 2010 +0200
@@ -1995,7 +1995,8 @@
   "solve goal by evaluation"
 
 method_setup normalization = {*
-  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))
+  Scan.succeed (K (SIMPLE_METHOD'
+    (CHANGED_PROP o CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))
 *} "solve goal by normalization"