--- a/src/CCL/Wfd.thy Thu Jul 30 11:23:17 2009 +0200
+++ b/src/CCL/Wfd.thy Thu Jul 30 11:23:57 2009 +0200
@@ -498,13 +498,14 @@
structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
in
-fun eval_tac ctxt ths i =
- DEPTH_SOLVE_1 (resolve_tac (ths @ Data.get ctxt) i ORELSE assume_tac i);
+fun eval_tac ths =
+ FOCUS_PREMS (fn {context, prems, ...} =>
+ DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
val eval_setup =
Data.setup #>
Method.setup @{binding eval}
- (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ctxt ths)))
+ (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt)))
"evaluation";
end;