FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;

--- 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;

--- a/src/HOL/Prolog/prolog.ML	Thu Jul 30 11:23:17 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML	Thu Jul 30 11:23:57 2009 +0200
@@ -67,7 +67,7 @@
         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
         imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
 
-(*val hyp_resolve_tac = FOCUS (fn {prems, ...} =>
+(*val hyp_resolve_tac = FOCUS_PREMS (fn {prems, ...} =>
                                   resolve_tac (maps atomizeD prems) 1);
   -- is nice, but cannot instantiate unknowns in the assumptions *)
 fun hyp_resolve_tac i st = let