changeset 60757 | c09598a97436 |
parent 60650 | 40eef52464f3 |
child 60817 | 3f38ed5a02c1 |
--- a/src/Provers/classical.ML Sat Jul 18 21:25:55 2015 +0200 +++ b/src/Provers/classical.ML Sat Jul 18 21:44:18 2015 +0200 @@ -157,7 +157,7 @@ val rule'' = rule' |> ALLGOALS (SUBGOAL (fn (goal, i) => if i = 1 orelse redundant_hyp goal - then eresolve0_tac [thin_rl] i + then eresolve_tac ctxt [thin_rl] i else all_tac)) |> Seq.hd |> Drule.zero_var_indexes;