diff -r d9e3e4c30d6b -r 29ba33d58637 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Thu Jan 25 09:32:34 2007 +0100
+++ b/src/HOL/Integ/IntArith.thy	Thu Jan 25 09:32:35 2007 +0100
@@ -448,7 +448,7 @@
      and "IntInf.-/ (_,/ 1))")
   (OCaml "_"
      and "Big'_int.big'_int'_of'_int/ 0"
-     and "Big'_int.big'_int'_of'_int/ -1"
+     and "Big'_int.big'_int'_of'_int/ (-1)"
      and "!(_; _; failwith \"BIT\")"
      and "Big'_int.succ'_big'_int"
      and "Big'_int.pred'_big'_int")