src/Pure/Isar/parse.ML

   val minus: string parser
   val term_var: string parser
   val type_ident: string parser
   val type_var: string parser
   val number: string parser
+  val float_number: string parser
   val string: string parser
   val alt_string: string parser
   val verbatim: string parser
   val sync: string parser
   val eof: string parser

   val opt_keyword: string -> bool parser
   val begin: string parser
   val opt_begin: bool parser
   val nat: int parser
   val int: int parser
+  val real: real parser
   val enum: string -> 'a parser -> 'a list parser
   val enum1: string -> 'a parser -> 'a list parser
   val and_list: 'a parser -> 'a list parser
   val and_list1: 'a parser -> 'a list parser
   val enum': string -> 'a context_parser -> 'a list context_parser

 val sym_ident = kind Token.SymIdent;
 val term_var = kind Token.Var;
 val type_ident = kind Token.TypeIdent;
 val type_var = kind Token.TypeVar;
 val number = kind Token.Nat;
+val float_number = kind Token.Float;
 val string = kind Token.String;
 val alt_string = kind Token.AltString;
 val verbatim = kind Token.Verbatim;
 val sync = kind Token.Sync;
 val eof = kind Token.EOF;

 val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
 fun maybe scan = underscore >> K NONE || scan >> SOME;
 
 val nat = number >> (#1 o Library.read_int o Symbol.explode);
 val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
+val real = float_number >> (the o Real.fromString);
 
 val tag_name = group "tag name" (short_ident || string);
 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
 
 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();