changeset 55990 | 41c6b99c5fb7 |
parent 55958 | 4ec984df4f45 |
child 56002 | 2028467b4df4 |
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 07 22:19:52 2014 +0100 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 07 22:30:58 2014 +0100 @@ -172,7 +172,7 @@ in (EVERY [DETERM tac, - REPEAT (etac ex1E 1), rtac ex1I 1, + REPEAT (etac @{thm ex1E} 1), rtac @{thm ex1I} 1, DEPTH_SOLVE_1 (ares_tac [intr] 1), REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1), etac elim 1,