| changeset 9653 | 2937a854e3d7 |
| parent 9631 | f4ebf1ec2df6 |
| child 9706 | 8e48a19fc81e |
--- a/src/Pure/Isar/method.ML Fri Aug 18 18:06:10 2000 +0200 +++ b/src/Pure/Isar/method.ML Fri Aug 18 18:11:10 2000 +0200 @@ -296,7 +296,7 @@ val resolveq_tac = gen_resolveq_tac Tactic.rtac; fun resolveq_cases_tac open_parms = gen_resolveq_tac (fn (rule, cases) => fn i => fn st => - Seq.map (rpair (RuleCases.make open_parms rule cases)) (Tactic.rtac rule i st)); + Seq.map (rpair (RuleCases.make (not open_parms) rule cases)) (Tactic.rtac rule i st)); (* simple rule *)