# HG changeset patch
# User haftmann
# Date 1309637687 -7200
# Node ID 905f17258bca0b7a38aa15c5bc3de3c9a3dfc449
# Parent  9cba66fb109ab57f794619989c19ea066d857612
tuned typo

diff -r 9cba66fb109a -r 905f17258bca src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Sat Jul 02 10:37:35 2011 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Sat Jul 02 22:14:47 2011 +0200
@@ -387,7 +387,7 @@
 *}
 
 code_const nat
-  (SML "IntInf.max/ (/0,/ _)")
+  (SML "IntInf.max/ (0,/ _)")
   (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
   (Eval "Integer.max/ _/ 0")