src/Pure/Syntax/lexicon.ML
changeset 5860 ed11c9890852
parent 5513 3896c7894a57
child 5868 0022d0a913b5
equal deleted inserted replaced
5859:87595fc95089 5860:ed11c9890852
    26   val var: indexname -> term
    26   val var: indexname -> term
    27   val binding: string -> string
    27   val binding: string -> string
    28   val dest_binding: string -> string
    28   val dest_binding: string -> string
    29   val skolem: string -> string
    29   val skolem: string -> string
    30   val dest_skolem: string -> string
    30   val dest_skolem: string -> string
       
    31   val read_nat: string -> int option
    31 end;
    32 end;
    32 
    33 
    33 signature LEXICON =
    34 signature LEXICON =
    34 sig
    35 sig
    35   include LEXICON0
    36   include LEXICON0
   332 
   333 
   333 val skolem = suffix "__";
   334 val skolem = suffix "__";
   334 val dest_skolem = unsuffix "__";
   335 val dest_skolem = unsuffix "__";
   335 
   336 
   336 
   337 
       
   338 (* read_nat *)
       
   339 
       
   340 fun read_nat str =
       
   341   (case Scan.finite Symbol.stopper (Scan.option scan_digits1) (Symbol.explode str) of
       
   342     (Some cs, []) => Some (#1 (Term.read_int cs))
       
   343   | _ => None);
       
   344 
       
   345 
   337 end;
   346 end;