# HG changeset patch
# User blanchet
# Date 1283410276 -7200
# Node ID e820beaf7d8cc60de099ea5179778f6247940528
# Parent  7cf8beb31e0fb1ab67fe6ee3e7ad3221cbacb6e5# Parent  c79e6d536267396bf82b0f033c1cf52bbd4e24ed
merged

diff -r c79e6d536267 -r e820beaf7d8c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Sep 02 08:29:30 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 02 08:51:16 2010 +0200
@@ -1996,7 +1996,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"