diff -r 429cfc5f2559 -r e7e41db7221b src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Mon Sep 26 07:56:54 2016 +0200
@@ -207,7 +207,7 @@
         pi
     | poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
         (p, Rat.add i m)
-    | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) (*DYNAMIC BINDING!*) $ t, m, pi as (p, i)) =
+    | poly (all as Const ("Num.numeral_class.numeral", _) (*DYNAMIC BINDING!*) $ t, m, pi as (p, i)) =
         (let val k = HOLogic.dest_numeral t
         in (p, Rat.add i (Rat.mult m (Rat.of_int k))) end
         handle TERM _ => add_atom all m pi)