src/HOL/Library/ML_Int.thy
changeset 24423 ae9cd0e92423
parent 24354 0fdabe28f0e6
child 24700 291665d063e4
     1.1 --- a/src/HOL/Library/ML_Int.thy	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/HOL/Library/ML_Int.thy	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -170,7 +170,7 @@
     1.4  
     1.5  setup {*
     1.6    CodeTarget.add_pretty_numeral "SML" false
     1.7 -    (@{const_name number_of}, @{typ "int \<Rightarrow> ml_int"})
     1.8 +    @{const_name ml_int_of_int}
     1.9      @{const_name Numeral.B0} @{const_name Numeral.B1}
    1.10      @{const_name Numeral.Pls} @{const_name Numeral.Min}
    1.11      @{const_name Numeral.Bit}