src/Provers/Arith/combine_numerals.ML

--- a/src/Provers/Arith/combine_numerals.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -68,7 +68,7 @@
 fun proc ctxt ct =
   let
     val t = Thm.term_of ct
-    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
 
     val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
     val T = Term.fastype_of u