--- a/src/HOL/Prolog/prolog.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML Thu Jul 30 12:20:43 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_PREMS (fn {prems, ...} =>
+(*val hyp_resolve_tac = Subgoal.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