# HG changeset patch
# User blanchet
# Date 1277476073 -7200
# Node ID cfc5e281740f8519134ec9b9a70fa257f57761c9
# Parent  b8c1f4c46983a88c94ee0969af9c581c3d2c83aa
exploit "Name.desymbolize" to remove some dependencies

diff -r b8c1f4c46983 -r cfc5e281740f src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 16:15:03 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 16:27:53 2010 +0200
@@ -186,6 +186,16 @@
 val min_wait_time = Time.fromMilliseconds 300;
 val max_wait_time = Time.fromSeconds 10;
 
+fun replace_all bef aft =
+  let
+    fun aux seen "" = String.implode (rev seen)
+      | aux seen s =
+        if String.isPrefix bef s then
+          aux seen "" ^ aft ^ aux [] (unprefix bef s)
+        else
+          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
+  in aux [] end
+
 (* This is a workaround for Proof General's off-by-a-few sendback display bug,
    whereby "pr" in "proof" is not highlighted. *)
 val break_into_chunks =
diff -r b8c1f4c46983 -r cfc5e281740f src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Jun 25 16:15:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Jun 25 16:27:53 2010 +0200
@@ -54,8 +54,6 @@
 structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
 struct
 
-open Sledgehammer_Util
-
 val type_wrapper_name = "ti"
 
 val schematic_var_prefix = "V_";
@@ -209,8 +207,7 @@
 
 fun readable_name full_name s =
   let
-    val s = s |> Long_Name.base_name
-              |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
+    val s = s |> Long_Name.base_name |> Name.desymbolize false
     val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
     val s' =
       (s' |> rev
diff -r b8c1f4c46983 -r cfc5e281740f src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jun 25 16:15:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jun 25 16:27:53 2010 +0200
@@ -8,8 +8,6 @@
 sig
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
-  val replace_all : string -> string -> string -> string
-  val remove_all : string -> string -> string
   val timestamp : unit -> string
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
@@ -31,17 +29,6 @@
   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
 
-fun replace_all bef aft =
-  let
-    fun aux seen "" = String.implode (rev seen)
-      | aux seen s =
-        if String.isPrefix bef s then
-          aux seen "" ^ aft ^ aux [] (unprefix bef s)
-        else
-          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
-  in aux [] end
-fun remove_all bef = replace_all bef ""
-
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
 
 fun parse_bool_option option name s =