src/HOL/Word/WordBitwise.thy
changeset 59058 a78612c67ec0
parent 57512 cc97b347b301
child 59498 50b60f501b05
--- 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