1.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -403,6 +403,6 @@
     1.4  
     1.5  fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
     1.6  
     1.7 -val setup = Try.register_tool (nitpickN, (auto, try_nitpick))
     1.8 +val setup = Try.register_tool (nitpickN, (50, auto, try_nitpick))
     1.9  
    1.10  end;

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
     2.3 @@ -414,6 +414,6 @@
     2.4                       (minimize_command [] i) state
     2.5    end
     2.6  
     2.7 -val setup = Try.register_tool (sledgehammerN, (auto, try_sledgehammer))
     2.8 +val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
     2.9  
    2.10  end;

     3.1 --- a/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
     3.2 +++ b/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
     3.3 @@ -182,6 +182,6 @@
     3.4  
     3.5  fun try_try_methods auto = do_try_methods auto NONE ([], [], [], [])
     3.6  
     3.7 -val setup = Try.register_tool (try_methodsN, (auto, try_try_methods))
     3.8 +val setup = Try.register_tool (try_methodsN, (20, auto, try_try_methods))
     3.9  
    3.10  end;

     4.1 --- a/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
     4.2 +++ b/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
     4.3 @@ -653,7 +653,7 @@
     4.4    end
     4.5    |> `(fn (outcome_code, _) => outcome_code = genuineN)
     4.6  
     4.7 -val setup = Try.register_tool (quickcheckN, (auto, try_quickcheck))
     4.8 +val setup = Try.register_tool (quickcheckN, (30, auto, try_quickcheck))
     4.9  
    4.10  end;
    4.11  

     5.1 --- a/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
     5.2 +++ b/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
     5.3 @@ -106,6 +106,6 @@
     5.4  
     5.5  (* hook *)
     5.6  
     5.7 -val setup = Try.register_tool (solve_directN, (auto, solve_direct));
     5.8 +val setup = Try.register_tool (solve_directN, (10, auto, solve_direct));
     5.9  
    5.10  end;

     6.1 --- a/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
     6.2 +++ b/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  signature TRY =
     6.5  sig
     6.6    type tool =
     6.7 -    string * (bool Unsynchronized.ref
     6.8 +    string * (int * bool Unsynchronized.ref
     6.9                * (bool -> Proof.state -> bool * (string * Proof.state)))
    6.10  
    6.11    val tryN : string
    6.12 @@ -22,7 +22,7 @@
    6.13  struct
    6.14  
    6.15  type tool =
    6.16 -  string * (bool Unsynchronized.ref
    6.17 +  string * (int * bool Unsynchronized.ref
    6.18              * (bool -> Proof.state -> bool * (string * Proof.state)))
    6.19  
    6.20  val tryN = "try"
    6.21 @@ -51,15 +51,16 @@
    6.22  
    6.23  val get_tools = Data.get
    6.24  
    6.25 -val register_tool = Data.map o AList.update (op =)
    6.26 +val register_tool = Data.map o Ord_List.insert (int_ord o pairself (#1 o snd))
    6.27  
    6.28  (* try command *)
    6.29  
    6.30  fun try_tools state =
    6.31    get_tools (Proof.theory_of state)
    6.32 -  |> tap (fn _ => Output.urgent_message "Trying...")
    6.33 +  |> tap (fn tools => "Trying " ^ commas_quote (map fst tools) ^ "..."
    6.34 +                      |> Output.urgent_message)
    6.35    |> Par_List.get_some
    6.36 -         (fn (name, (_, tool)) =>
    6.37 +         (fn (name, (_, _, tool)) =>
    6.38               case try (tool false) state of
    6.39                 SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
    6.40               | _ => NONE)
    6.41 @@ -74,7 +75,7 @@
    6.42  
    6.43  fun auto_try state =
    6.44    get_tools (Proof.theory_of state)
    6.45 -  |> map_filter (fn (_, (auto, tool)) => if !auto then SOME tool else NONE)
    6.46 +  |> map_filter (fn (_, (_, auto, tool)) => if !auto then SOME tool else NONE)
    6.47    |> Par_List.get_some (fn tool =>
    6.48                             case try (tool true) state of
    6.49                               SOME (true, (_, state)) => SOME state