# HG changeset patch
# User blanchet
# Date 1280437895 -7200
# Node ID 019a49759829856c5d400622f662865edf9b405b
# Parent  34b75b71235d0b2a405bee8fc667a665ad136a60
fix bug in the newly introduced "bound concealing" code

diff -r 34b75b71235d -r 019a49759829 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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