# HG changeset patch
# User wenzelm
# Date 1248630877 -7200
# Node ID 752dbe71cc890c8d3f2ad6d3e55c4ceeb9f7bdce
# Parent  a5e9d9f3e5e123150c8380a45952d057f9a45300
tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);

diff -r a5e9d9f3e5e1 -r 752dbe71cc89 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Sun Jul 26 19:38:02 2009 +0200
+++ b/src/CCL/Wfd.thy	Sun Jul 26 19:54:37 2009 +0200
@@ -498,14 +498,13 @@
   structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
 in
 
-fun eval_tac ctxt ths =
-  METAHYPS (fn prems =>
-    DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get ctxt) 1)) 1;
+fun eval_tac ctxt ths i =
+  DEPTH_SOLVE_1 (resolve_tac (ths @ Data.get ctxt) i ORELSE assume_tac i);
 
 val eval_setup =
   Data.setup #>
   Method.setup @{binding eval}
-    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))))
+    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ctxt ths)))
     "evaluation";
 
 end;