1.1 --- a/src/HOL/HOL.thy	Tue Dec 14 00:16:30 2010 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Dec 15 09:47:12 2010 +0100
     1.3 @@ -1976,7 +1976,7 @@
     1.4  
     1.5  method_setup normalization = {*
     1.6    Scan.succeed (K (SIMPLE_METHOD'
     1.7 -    (CHANGED_PROP o (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k))))))
     1.8 +    (CHANGED_PROP o (CONVERSION Nbe.dynamic_conv THEN' (fn k => TRY (rtac TrueI k))))))
     1.9  *} "solve goal by normalization"
    1.10  
    1.11