src/HOL/Code_Setup.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
     1.1 --- a/src/HOL/Code_Setup.thy	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/Code_Setup.thy	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -226,19 +226,19 @@
     1.4  *}
     1.5  
     1.6  ML {*
     1.7 -fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD'
     1.8 +fun gen_eval_method conv ctxt = SIMPLE_METHOD'
     1.9    (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
    1.10 -    THEN' rtac TrueI))
    1.11 +    THEN' rtac TrueI)
    1.12  *}
    1.13  
    1.14 -method_setup eval = {* gen_eval_method eval_oracle *}
    1.15 +method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
    1.16    "solve goal by evaluation"
    1.17  
    1.18 -method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
    1.19 +method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
    1.20    "solve goal by evaluation"
    1.21  
    1.22 -method_setup normalization = {* (Method.no_args o SIMPLE_METHOD')
    1.23 -  (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
    1.24 +method_setup normalization = {*
    1.25 +  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
    1.26  *} "solve goal by normalization"
    1.27  
    1.28