diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -320,7 +320,7 @@
   (case Item_Net.content (get_functions ctxt) of
     [] => NONE
   | (t, _) :: _ =>
-      let val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+      let val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
       in import_function_data t' ctxt' end)