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
no_document use_thys [
"~~/src/HOL/Library/Infinite_Set",
"~~/src/HOL/Library/Permutation"
];
use_thys [
"Fib",
"Factorization",
"Chinese",
"WilsonRuss",
"WilsonBij",
"Quadratic_Reciprocity",
"Primes",
"Pocklington"
];