src/Pure/General/symbol_pos.ML

--- a/src/Pure/General/symbol_pos.ML	Thu Mar 31 15:42:01 2016 +0200
+++ b/src/Pure/General/symbol_pos.ML	Thu Mar 31 16:23:25 2016 +0200
@@ -46,6 +46,8 @@
   val explode0: string -> T list
   val scan_ident: T list -> T list * T list
   val is_identifier: string -> bool
+  val scan_nat: T list -> T list * T list
+  val scan_float: T list -> T list * T list
 end;
 
 structure Symbol_Pos: SYMBOL_POS =
@@ -300,6 +302,12 @@
       SOME (_, []) => true
     | _ => false);
 
+
+(* numerals *)
+
+val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
+val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat;
+
 end;
 
 structure Basic_Symbol_Pos =   (*not open by default*)