--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed May 15 18:44:19 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed May 15 23:00:17 2013 +0200
@@ -45,9 +45,11 @@
val auto = Unsynchronized.ref false
val _ =
- ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.bool_pref auto "auto-sledgehammer"
- "Run Sledgehammer automatically.")
+ ProofGeneral.preference_bool ProofGeneral.category_tracing
+ NONE
+ auto
+ "auto-sledgehammer"
+ "Run Sledgehammer automatically"
(** Sledgehammer commands **)
@@ -66,16 +68,18 @@
val timeout = Unsynchronized.ref 30
val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.string_pref provers
- "Sledgehammer: Provers"
- "Default automatic provers (separated by whitespace)")
+ ProofGeneral.preference_string ProofGeneral.category_proof
+ NONE
+ provers
+ "Sledgehammer: Provers"
+ "Default automatic provers (separated by whitespace)"
val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.int_pref timeout
- "Sledgehammer: Time Limit"
- "ATPs will be interrupted after this time (in seconds)")
+ ProofGeneral.preference_int ProofGeneral.category_proof
+ NONE
+ timeout
+ "Sledgehammer: Time Limit"
+ "ATPs will be interrupted after this time (in seconds)"
type raw_param = string * string list