fixed detection of Skolem constants in type construction detection code
header {* Plain HOL *}theory Plainimports Datatype FunDef Extraction Metisbegintext {* Plain bootstrap of fundamental HOL tools and packages; does not include @{text Hilbert_Choice}.*}end