src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -43,7 +43,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_sledgehammer}
+    @{system_option auto_sledgehammer}
     "auto-sledgehammer"
     "Run Sledgehammer automatically"
 
@@ -72,7 +72,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_proof
     NONE
-    @{option sledgehammer_timeout}
+    @{system_option sledgehammer_timeout}
     "Sledgehammer: Time Limit"
     "ATPs will be interrupted after this time (in seconds)"
 
@@ -229,7 +229,7 @@
     |> fold (AList.default (op =))
          [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),
           ("timeout",
-           let val timeout = Options.default_int @{option sledgehammer_timeout} in
+           let val timeout = Options.default_int @{system_option sledgehammer_timeout} in
              [if timeout <= 0 then "none" else string_of_int timeout]
            end)]
   end
@@ -472,7 +472,7 @@
       state
   end
 
-val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
+val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
 
 val _ =
   Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>