src/HOL/Tools/ATP/recon_parse.ML
changeset 16804 3c339e1c069b
parent 16548 aa36ae6b955e
child 16840 3d5aad11bc24
equal deleted inserted replaced
16803:014090d1e64b 16804:3c339e1c069b
     9 (* Auxiliary functions *)
     9 (* Auxiliary functions *)
    10 
    10 
    11 structure Recon_Parse =
    11 structure Recon_Parse =
    12 struct
    12 struct
    13 
    13 
    14 exception ASSERTION of string;
    14 open ReconPrelim ReconTranslateProof;
    15 
    15 
    16 exception NOPARSE_WORD
    16 exception NOPARSE_WORD
    17 exception NOPARSE_NUM
    17 exception NOPARSE_NUM
    18 fun to_upper s = String.translate (Char.toString o Char.toUpper) s;
    18 fun to_upper s = String.translate (Char.toString o Char.toUpper) s;
    19 
    19 
    20 fun string2int s =
    20 fun string2int s =
    21   let
    21   (case Int.fromString s of SOME i => i
    22     val io = Int.fromString s
    22   | NONE => raise ASSERTION "string -> int failed");
    23   in
    23 
    24     case io of
       
    25       (SOME i) => i
       
    26       | _ => raise ASSERTION "string -> int failed"
       
    27   end
       
    28 
    24 
    29 (* Parser combinators *)
    25 (* Parser combinators *)
    30 
    26 
    31 exception Noparse;
    27 exception Noparse;
    32 exception SPASSError of string;
    28 exception SPASSError of string;