| changeset 58837 | e84d900cd287 |
| parent 56438 | 7f6b2634d853 |
| child 59498 | 50b60f501b05 |
--- a/src/Pure/skip_proof.ML Thu Oct 30 16:17:56 2014 +0100 +++ b/src/Pure/skip_proof.ML Thu Oct 30 16:20:46 2014 +0100 @@ -38,6 +38,6 @@ (* cheat_tac *) fun cheat_tac i st = - rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st; + resolve_tac [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st; end;