changeset 32283 | 3bebc195c124 |
parent 32262 | 73cd8f74cf2a |
child 32740 | 9dd0a2f83429 |
--- a/src/HOL/Tools/res_axioms.ML Thu Jul 30 11:23:57 2009 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Jul 30 12:20:43 2009 +0200 @@ -517,7 +517,7 @@ SUBGOAL (fn (prop, i) => let val ts = Logic.strip_assums_hyp prop in EVERY' - [FOCUS + [Subgoal.FOCUS (fn {prems, ...} => (Method.insert_tac (map forall_intr_vars (neg_clausify prems)) i)) ctxt,