src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed Jul 04 14:21:00 2007 +0200
+++ b/src/HOL/HOL.thy	Wed Jul 04 16:49:34 2007 +0200
@@ -1674,7 +1674,8 @@
 
 method_setup normalization = {*
   Method.no_args (Method.SIMPLE_METHOD'
-    (CONVERSION (HOLogic.Trueprop_conv NBE.normalization_conv) THEN' resolve_tac [TrueI, refl]))
+    (CONVERSION (ObjectLogic.judgment_conv NBE.normalization_conv)
+      THEN' resolve_tac [TrueI, refl]))
 *} "solve goal by normalization"