# HG changeset patch
# User chaieb
# Date 1181674196 -7200
# Node ID b8139ba0c940ca8c4d85bfac7b4a14bf5f509e67
# Parent  fb48c590dee18556b42a787fa2f0f13b25f72fe6
Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns

diff -r fb48c590dee1 -r b8139ba0c940 src/HOL/Tools/Presburger/generated_cooper.ML
--- a/src/HOL/Tools/Presburger/generated_cooper.ML	Tue Jun 12 20:49:50 2007 +0200
+++ b/src/HOL/Tools/Presburger/generated_cooper.ML	Tue Jun 12 20:49:56 2007 +0200
@@ -1,6 +1,6 @@
 structure GeneratedCooper =
 struct
-
+nonfix oo;
 fun nat i = if i < 0 then 0 else i;
 
 val one_def0 : int = (0 + 1);