src/HOL/Code_Setup.thy
changeset 25866 263aaf988d44
parent 25860 844ab7ace3db
child 25885 6fbc3f54f819
     1.1 --- a/src/HOL/Code_Setup.thy	Tue Jan 08 11:37:32 2008 +0100
     1.2 +++ b/src/HOL/Code_Setup.thy	Tue Jan 08 11:37:37 2008 +0100
     1.3 @@ -145,8 +145,9 @@
     1.4  
     1.5  method_setup normalization = {*
     1.6    Method.no_args (Method.SIMPLE_METHOD'
     1.7 -    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
     1.8 -      THEN' resolve_tac [TrueI, refl]))
     1.9 +    (fn k => CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) k
    1.10 +    THEN TRYALL (resolve_tac [TrueI])
    1.11 +  ))
    1.12  *} "solve goal by normalization"
    1.13  
    1.14  end