# HG changeset patch
# User blanchet
# Date 1284679321 -7200
# Node ID d91ef7fbc5004b9a7fe96f225823e028715d4eee
# Parent  40bf0f66b994cf31e51b68fded80a4cdf77dba19
move functions around

diff -r 40bf0f66b994 -r d91ef7fbc500 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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 **)
 
diff -r 40bf0f66b994 -r d91ef7fbc500 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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