src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 04 20:49:33 2019 +0200
@@ -1251,7 +1251,7 @@
       else
         let (*Norbert Schirmer's case*)
           val t = Thm.term_of ct;
-          val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
+          val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt;
         in
           Option.map (hd o Variable.export ctxt' ctxt o single)
             (case t' of Const (\<^const_name>\<open>Let\<close>,_) $ x $ f => (* x and f are already in normal form *)