--- a/src/HOL/Tools/SMT2/smtlib2.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2.ML Thu Jun 12 01:00:49 2014 +0200
@@ -17,7 +17,7 @@
val parse: string list -> tree
val pretty_tree: tree -> Pretty.T
val str_of: tree -> string
-end
+end;
structure SMTLIB2: SMTLIB2 =
struct
@@ -37,7 +37,6 @@
datatype unfinished = None | String of string | Symbol of string
-
(* utilities *)
fun read_raw pred l cs =
@@ -47,7 +46,6 @@
| x => x)
-
(* numerals and decimals *)
fun int_of cs = fst (read_int cs)
@@ -60,7 +58,6 @@
| (cs1, cs2) => (Num (int_of cs1), cs2))
-
(* binary numbers *)
fun is_bin c = (c = "0" orelse c = "1")
@@ -68,7 +65,6 @@
fun read_bin l cs = read_raw is_bin l cs |>> Num o fst o read_radix_int 2
-
(* hex numbers *)
val is_hex = member (op =) (raw_explode "0123456789abcdefABCDEF")
@@ -85,7 +81,6 @@
fun read_hex l cs = read_raw is_hex l cs |>> Num o unhex 0
-
(* symbols *)
val symbol_chars = raw_explode "~!@$%^&*_+=<>.?/-"
@@ -98,7 +93,6 @@
fun read_sym f l cs = read_raw is_sym l cs |>> f o implode
-
(* quoted tokens *)
fun read_quoted stop (escape, replacement) cs =
@@ -116,7 +110,6 @@
fun read_symbol cs = read_quoted ["|"] ([], "") cs
-
(* core parser *)
fun read _ [] rest tss = (rest, tss)
@@ -172,7 +165,6 @@
fun parse lines = finish (fold add_line lines (1, (None, [[]])))
-
(* pretty printer *)
fun pretty_tree (Num i) = Pretty.str (string_of_int i)
@@ -196,4 +188,4 @@
val str_of = Pretty.str_of o pretty_tree
-end
+end;