--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 22:57:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 23:11:35 2010 +0200
@@ -69,8 +69,13 @@
(** The Sledgehammer **)
+(* Identifier to distinguish Sledgehammer from other tools using
+ "Async_Manager". *)
val das_Tool = "Sledgehammer"
+(* Freshness almost guaranteed! *)
+val sledgehammer_weak_prefix = "Sledgehammer:"
+
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
val messages = Async_Manager.thread_messages das_Tool "ATP"
@@ -234,11 +239,10 @@
#> Meson.presimplify
#> prop_of
-(* Freshness almost guaranteed! *)
-fun concealed_bound_name j = das_Tool ^ Int.toString j
+fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
fun conceal_bounds Ts t =
subst_bounds (map (Free o apfst concealed_bound_name)
- (length Ts - 1 downto 0 ~~ rev Ts), t)
+ (0 upto length Ts - 1 ~~ Ts), t)
fun reveal_bounds Ts =
subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
(0 upto length Ts - 1 ~~ Ts))
@@ -287,7 +291,7 @@
fun aux (t $ u) = aux t $ aux u
| aux (Abs (s, T, t)) = Abs (s, T, aux t)
| aux (Var ((s, i), T)) =
- Free (das_Tool ^ "_" ^ s ^ "_" ^ string_of_int i, T)
+ Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
| aux t = t
in t |> exists_subterm is_Var t ? aux end