# HG changeset patch
# User haftmann
# Date 1169713955 -3600
# Node ID 29ba33d58637a71db7c4023b8d5b23e7043f7756
# Parent  d9e3e4c30d6bcb97640bcca52e5c723bea8cc909
fxied bug for OCaml bigints

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")