# 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 *)