src/HOL/Library/Efficient_Nat.thy
changeset 43653 905f17258bca
parent 43324 2b47822868e4
child 45185 3a0c63c0ed48
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Sat Jul 02 10:37:35 2011 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Sat Jul 02 22:14:47 2011 +0200
     1.3 @@ -387,7 +387,7 @@
     1.4  *}
     1.5  
     1.6  code_const nat
     1.7 -  (SML "IntInf.max/ (/0,/ _)")
     1.8 +  (SML "IntInf.max/ (0,/ _)")
     1.9    (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
    1.10    (Eval "Integer.max/ _/ 0")
    1.11