--- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Jun 04 20:49:33 2019 +0200
@@ -346,8 +346,8 @@
| _ => false) fully_skolemized_t then
let
val (fully_skolemized_ct, ctxt) =
- Variable.import_terms true [fully_skolemized_t] ctxt
- |>> the_single |>> Thm.cterm_of ctxt
+ yield_singleton (Variable.import_terms true) fully_skolemized_t ctxt
+ |>> Thm.cterm_of ctxt
in
(SOME (discharger_th, fully_skolemized_ct),
(Thm.assume fully_skolemized_ct, ctxt))