1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 10:30:53 2010 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 10:30:53 2010 +0200
     1.3 @@ -317,7 +317,7 @@
     1.4      else error("Int value too big:" + this.value.toString)
     1.5  
     1.6    def +(that: Nat): Nat = new Nat(this.value + that.value)
     1.7 -  def -(that: Nat): Nat = Nat(this.value + that.value)
     1.8 +  def -(that: Nat): Nat = Nat(this.value - that.value)
     1.9    def *(that: Nat): Nat = new Nat(this.value * that.value)
    1.10  
    1.11    def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)