src/Sequents/simpdata.ML

   |> Simplifier.set_subgoaler asm_simp_tac
   |> Simplifier.set_mksimps (K (map mk_meta_eq o atomize o gen_all))
   |> Simplifier.set_mkcong mk_meta_cong;
 
 val LK_simps =
-   [triv_forall_equality, (* prunes params *)
+   [@{thm triv_forall_equality}, (* prunes params *)
     @{thm refl} RS @{thm P_iff_T}] @
     @{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @
     @{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @
     @{thms all_simps} @ @{thms ex_simps} @
     [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @