# HG changeset patch
# User wenzelm
# Date 1326312262 -3600
# Node ID a42c5f23109f0512a61f9a545da66a810f1c9733
# Parent  7f6668317e2491fb33f7fa3888cbc62514c2964c
more conventional eval_tac vs. method_setup "eval";
clarified method "normalization": THEN_ALL_NEW avoids bumping into other subgoals;

diff -r 7f6668317e24 -r a42c5f23109f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jan 11 18:02:59 2012 +0100
+++ b/src/HOL/HOL.thy	Wed Jan 11 21:04:22 2012 +0100
@@ -1906,19 +1906,20 @@
 subsubsection {* Evaluation and normalization by evaluation *}
 
 ML {*
-fun gen_eval_method conv ctxt = SIMPLE_METHOD'
-  (CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 (conv ctxt))) ctxt)
-    THEN' rtac TrueI)
+fun eval_tac ctxt =
+  let val conv = Code_Runtime.dynamic_holds_conv (Proof_Context.theory_of ctxt)
+  in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
 *}
 
-method_setup eval = {*
-  Scan.succeed (gen_eval_method (Code_Runtime.dynamic_holds_conv o Proof_Context.theory_of))
-*} "solve goal by evaluation"
+method_setup eval = {* Scan.succeed (SIMPLE_METHOD' o eval_tac) *}
+  "solve goal by evaluation"
 
 method_setup normalization = {*
-  Scan.succeed (fn ctxt => SIMPLE_METHOD'
-    (CHANGED_PROP o (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))
-      THEN' (fn k => TRY (rtac TrueI k)))))
+  Scan.succeed (fn ctxt =>
+    SIMPLE_METHOD'
+      (CHANGED_PROP o
+        (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))
+          THEN_ALL_NEW (TRY o rtac TrueI))))
 *} "solve goal by normalization"