Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
(* Title: HOL/SizeChange/ROOT.ML
ID: $Id$
*)
no_document use_thy "Infinite_Set";
no_document use_thy "Ramsey";
use_thy "Examples";