normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 21:11:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun May 29 19:40:56 2011 +0200
@@ -189,7 +189,7 @@
   let
     val ctxt = Proof.context_of state
     val reserved = reserved_isar_keyword_table ()
-    val chained_ths = #facts (Proof.goal state)
+    val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
     val facts =
       refs
       |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 21:11:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 29 19:40:56 2011 +0200
@@ -146,7 +146,7 @@
                       reraise exn
                     else
                       (unknownN, "Internal error:\n" ^
-                                ML_Compiler.exn_message exn ^ "\n"))
+                                 ML_Compiler.exn_message exn ^ "\n"))
         val _ =
           (* The "expect" argument is deliberately ignored if the prover is
              missing so that the "Metis_Examples" can be processed on any
@@ -183,7 +183,7 @@
       end
     else
       (Async_Manager.launch das_tool birth_time death_time (desc ())
-                            (apfst (curry (op <>) timeoutN) o go);
+                            (apfst (curry (op =) someN) o go);
        (unknownN, state))
   end
 
@@ -191,7 +191,8 @@
   ctxt |> select_smt_solver name
        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
 
-(* Makes backtraces more transparent and might be more efficient as well. *)
+(* Makes backtraces more transparent and might well be more efficient as
+   well. *)
 fun smart_par_list_map _ [] = []
   | smart_par_list_map f [x] = [f x]
   | smart_par_list_map f xs = Par_List.map f xs
@@ -217,6 +218,7 @@
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
       val {facts = chained_ths, goal, ...} = Proof.goal state
+      val chained_ths = chained_ths |> normalize_chained_theorems
       val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
@@ -318,7 +320,7 @@
       val launch_ueq_atps =
         launch_atps "Unit equational provers" is_unit_equality ueq_atps
       fun launch_atps_and_smt_solvers () =
-        [launch_full_atps, launch_ueq_atps, launch_smts]
+        [launch_full_atps, launch_smts, launch_ueq_atps]
         |> smart_par_list_map (fn f => ignore (f (unknownN, state)))
         handle ERROR msg => (print ("Error: " ^ msg); error msg)
       fun maybe f (accum as (outcome_code, _)) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 21:11:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sun May 29 19:40:56 2011 +0200
@@ -31,6 +31,7 @@
   val subgoal_count : Proof.state -> int
   val strip_subgoal :
     Proof.context -> thm -> int -> (string * typ) list * term list * term
+  val normalize_chained_theorems : thm list -> thm list
   val reserved_isar_keyword_table : unit -> unit Symtab.table
 end;
 
@@ -253,6 +254,8 @@
     val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
   in (rev params, hyp_ts, concl_t) end
 
+val normalize_chained_theorems =
+  maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
 fun reserved_isar_keyword_table () =
   union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
   |> map (rpair ()) |> Symtab.make