fixed type annotation
authorhaftmann
Thu Sep 15 08:16:22 2005 +0200 (2005-09-15)
changeset 174019147c880ada6
parent 17400 6ede71a506f5
child 17402 41f1249bce37
fixed type annotation
src/HOL/Integ/reflected_presburger.ML
src/HOL/Tools/Presburger/reflected_presburger.ML
     1.1 --- a/src/HOL/Integ/reflected_presburger.ML	Thu Sep 15 07:35:38 2005 +0200
     1.2 +++ b/src/HOL/Integ/reflected_presburger.ML	Thu Sep 15 08:16:22 2005 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  
     1.5      (* Caution: This file should not be modified. *)
     1.6      (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
     1.7 -fun (nat: IntInf.int -> IntInf.int) i = if i < 0 then 0 else i;
     1.8 +fun nat (i:IntInf.int) = if i < 0 then 0 else i : IntInf.int;
     1.9  structure Generated =
    1.10  struct
    1.11  
     2.1 --- a/src/HOL/Tools/Presburger/reflected_presburger.ML	Thu Sep 15 07:35:38 2005 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/reflected_presburger.ML	Thu Sep 15 08:16:22 2005 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4  
     2.5      (* Caution: This file should not be modified. *)
     2.6      (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
     2.7 -fun (nat: IntInf.int -> IntInf.int) i = if i < 0 then 0 else i;
     2.8 +fun nat (i:IntInf.int) = if i < 0 then 0 else i : IntInf.int;
     2.9  structure Generated =
    2.10  struct
    2.11