# HG changeset patch
# User haftmann
# Date 1215533589 -7200
# Node ID f56684dd75a5c7b0dd11c81cd47a16a9f4b1fe7b
# Parent  d2bb5d61b392c89cc36cb636259e14ba2f7a731e
fix: using IntInf.int for SML

diff -r d2bb5d61b392 -r f56684dd75a5 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 08 17:52:28 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 08 18:13:09 2008 +0200
@@ -241,7 +241,7 @@
 *}
 
 code_type nat
-  (SML "int")
+  (SML "IntInf.int")
   (OCaml "Big'_int.big'_int")
 
 types_code