src/Pure/Isar/parse.ML
changeset 40296 ac4d75f86d97
parent 40290 47f572aff50a
child 40793 d21aedaa91e7
     1.1 --- a/src/Pure/Isar/parse.ML	Sun Oct 31 11:45:45 2010 +0100
     1.2 +++ b/src/Pure/Isar/parse.ML	Sun Oct 31 13:26:37 2010 +0100
     1.3 @@ -195,7 +195,7 @@
     1.4  
     1.5  val nat = number >> (#1 o Library.read_int o Symbol.explode);
     1.6  val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
     1.7 -val real = float_number >> (the o Real.fromString);
     1.8 +val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
     1.9  
    1.10  val tag_name = group "tag name" (short_ident || string);
    1.11  val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);