diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Word/WordBitwise.thy --- a/src/HOL/Word/WordBitwise.thy Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Word/WordBitwise.thy Wed Nov 26 20:05:34 2014 +0100 @@ -510,7 +510,7 @@ case term_of ct of (@{const upt} $ n $ m) => let - val (i, j) = pairself (snd o HOLogic.dest_number) (n, m); + val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m); val ns = map (Numeral.mk_cnumber @{ctyp nat}) (i upto (j - 1)) |> mk_nat_clist; val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns