changeset 32282 | 853ef99c04cc |
parent 32260 | eb97888fa422 |
child 32283 | 3bebc195c124 |
--- 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