--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 17 00:54:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 17 01:22:01 2010 +0200
@@ -43,6 +43,13 @@
string Symtab.table * bool * int * Proof.context * int list list
type text_result = string * (string * locality) list
+fun is_head_digit s = Char.isDigit (String.sub (s, 0))
+val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
+
+fun find_first_in_list_vector vec key =
+ Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
+ | (_, value) => value) NONE vec
+
(** SPASS's Flotter hack **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Sep 17 00:54:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Sep 17 01:22:01 2010 +0200
@@ -6,13 +6,11 @@
signature SLEDGEHAMMER_UTIL =
sig
- val find_first_in_list_vector : (''a * 'b) list vector -> ''a -> 'b option
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
- val scan_integer : string list -> int * string list
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
@@ -28,10 +26,6 @@
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
-fun find_first_in_list_vector vec key =
- Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
- | (_, value) => value) NONE vec
-
fun plural_s n = if n = 1 then "" else "s"
fun serial_commas _ [] = ["??"]
@@ -72,9 +66,6 @@
SOME (Time.fromMilliseconds msecs)
end
-fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
-
val subscript = implode o map (prefix "\<^isub>") o explode
fun nat_subscript n =
n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript