Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Code_Setup.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85 
--- a/src/HOL/Code_Setup.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Code_Setup.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -226,19 +226,19 @@
 *}
 
 ML {*
-fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD'
+fun gen_eval_method conv ctxt = SIMPLE_METHOD'
   (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
-    THEN' rtac TrueI))
+    THEN' rtac TrueI)
 *}
 
-method_setup eval = {* gen_eval_method eval_oracle *}
+method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
   "solve goal by evaluation"
 
-method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
+method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
   "solve goal by evaluation"
 
-method_setup normalization = {* (Method.no_args o SIMPLE_METHOD')
-  (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
+method_setup normalization = {*
+  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
 *} "solve goal by normalization"
isabelle