changeset 43653 | 905f17258bca |
parent 43324 | 2b47822868e4 |
child 45185 | 3a0c63c0ed48 |
--- 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")