src/HOL/Tools/Datatype/rep_datatype.ML

           let
             val k = length (filter Datatype_Aux.is_rec_type cargs);
           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,
                 REPEAT_DETERM_N j distinct_tac,
                 TRY (dresolve_tac inject 1),