# HG changeset patch
# User wenzelm
# Date 966615070 -7200
# Node ID 2937a854e3d724baa648fa79370fdf234ca7ad74
# Parent  ea1f02d6d65b9ca66ad1c92af8113102e0dcdb7e
fixed RuleCases.make (invert flag);

diff -r ea1f02d6d65b -r 2937a854e3d7 src/Pure/Isar/method.ML
--- 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 *)