# HG changeset patch
# User blanchet
# Date 1273828809 -7200
# Node ID fb18db78be80c6a20935dfd31a13526cc369642a
# Parent  9063a5b2b2bbc55aa96a3001a26fd9cff054ede9
delect installed ATPs dynamically, _not_ at image built time

diff -r 9063a5b2b2bb -r fb18db78be80 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 13 15:09:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 14 11:20:09 2010 +0200
@@ -64,7 +64,7 @@
 
 (*** parameters ***)
 
-val atps = Unsynchronized.ref (default_atps_param_value ())
+val atps = Unsynchronized.ref ""
 val timeout = Unsynchronized.ref 60
 val full_types = Unsynchronized.ref false
 
@@ -112,7 +112,7 @@
    ("ignore_no_atp", "respect_no_atp"),
    ("theory_irrelevant", "theory_relevant"),
    ("dont_follow_defs", "follow_defs"),
-   ("metis_proof", "isar_proof")]
+   ("no_isar_proof", "isar_proof")]
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "full_types", "explicit_apply",
@@ -152,7 +152,7 @@
 fun default_raw_params thy =
   Data.get thy
   |> fold (AList.default (op =))
-          [("atps", [!atps]),
+          [("atps", [case !atps of "" => default_atps_param_value () | s => s]),
            ("full_types", [if !full_types then "true" else "false"]),
            ("timeout", let val timeout = !timeout in
                          [if timeout <= 0 then "none"