src/HOL/Tools/quickcheck_generators.ML

           let
             val proj_simps = map (snd o snd) proj_defs;
             fun tac { context = ctxt, prems = _ } =
               ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
               THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
-              THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
+              THEN ALLGOALS (simp_tac (HOL_ss addsimps [@{thm fst_conv}, @{thm snd_conv}]));
           in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
       in
         lthy
         |> random_aux_primrec aux_eq'
         ||>> fold_map Local_Theory.define proj_defs