fixed RuleCases.make (invert flag);
authorwenzelm
Fri Aug 18 18:11:10 2000 +0200 (2000-08-18)
changeset 96532937a854e3d7
parent 9652 ea1f02d6d65b
child 9654 9754ba005b64
fixed RuleCases.make (invert flag);
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Fri Aug 18 18:06:10 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Aug 18 18:11:10 2000 +0200
     1.3 @@ -296,7 +296,7 @@
     1.4  val resolveq_tac = gen_resolveq_tac Tactic.rtac;
     1.5  
     1.6  fun resolveq_cases_tac open_parms = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
     1.7 -  Seq.map (rpair (RuleCases.make open_parms rule cases)) (Tactic.rtac rule i st));
     1.8 +  Seq.map (rpair (RuleCases.make (not open_parms) rule cases)) (Tactic.rtac rule i st));
     1.9  
    1.10  
    1.11  (* simple rule *)