src/HOL/HOLCF/IMP/ROOT.ML

gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings

use_thys ["HoareEx"];