# HG changeset patch # User wenzelm # Date 1121263645 -7200 # Node ID 3c339e1c069bb3cd6c0d9220f5c1ba7a051794fd # Parent 014090d1e64b1b4113b9288d92d91987f77895e1 open ReconPrelim ReconTranslateProof; removed second copy of exception ASSERTION; diff -r 014090d1e64b -r 3c339e1c069b src/HOL/Tools/ATP/recon_parse.ML --- a/src/HOL/Tools/ATP/recon_parse.ML Wed Jul 13 16:07:24 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_parse.ML Wed Jul 13 16:07:25 2005 +0200 @@ -11,20 +11,16 @@ structure Recon_Parse = struct -exception ASSERTION of string; +open ReconPrelim ReconTranslateProof; exception NOPARSE_WORD exception NOPARSE_NUM fun to_upper s = String.translate (Char.toString o Char.toUpper) s; fun string2int s = - let - val io = Int.fromString s - in - case io of - (SOME i) => i - | _ => raise ASSERTION "string -> int failed" - end + (case Int.fromString s of SOME i => i + | NONE => raise ASSERTION "string -> int failed"); + (* Parser combinators *)