--- a/src/HOL/TPTP/atp_problem_import.ML Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Thu Nov 21 19:13:49 2013 +0100
@@ -309,11 +309,11 @@
val (format, type_enc, lam_trans) =
(case format_str of
"FOF" => (FOF, "mono_guards??", liftingN)
- | "TFF0" => (TFF Monomorphic, "mono_native", liftingN)
- | "THF0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
+ | "TF0" => (TFF Monomorphic, "mono_native", liftingN)
+ | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
| "DFG" => (DFG Monomorphic, "mono_native", liftingN)
| _ => error ("Unknown format " ^ quote format_str ^
- " (expected \"FOF\", \"TFF0\", \"THF0\", or \"DFG\")"))
+ " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
val uncurried_aliases = false
val readable_names = true
val presimp = true
--- a/src/HOL/TPTP/lib/Tools/tptp_translate Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate Thu Nov 21 19:13:49 2013 +0100
@@ -11,7 +11,7 @@
echo
echo "Usage: isabelle $PRG FORMAT FILE"
echo
- echo " Translates TPTP input file to the specified format (\"FOF\", \"TFF0\", \"THF0\", or \"DFG\")."
+ echo " Translates TPTP input file to the specified format (\"FOF\", \"TF0\", \"TH0\", or \"DFG\")."
echo " Emits the result to standard output."
echo
exit 1
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Nov 21 19:13:49 2013 +0100
@@ -144,10 +144,7 @@
structure Data = Theory_Data
(
type T = raw_param list
- val empty =
- default_default_params
- |> getenv "NITPICK_SPY" = "yes" ? AList.update (op =) ("spy", "true")
- |> map (apsnd single)
+ val empty = default_default_params |> map (apsnd single)
val extend = I
fun merge data = AList.merge (op =) (K true) data
)
@@ -258,7 +255,7 @@
val debug = (mode <> Auto_Try andalso lookup_bool "debug")
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
- val spy = lookup_bool "spy"
+ val spy = getenv "NITPICK_SPY" = "yes" orelse lookup_bool "spy"
val user_axioms = lookup_bool_option "user_axioms"
val assms = lookup_bool "assms"
val whacks = lookup_term_list_option_polymorphic "whack" |> these
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Nov 21 19:13:49 2013 +0100
@@ -187,10 +187,7 @@
structure Data = Theory_Data
(
type T = raw_param list
- val empty =
- default_default_params
- |> getenv "SLEDGEHAMMER_SPY" = "yes" ? AList.update (op =) ("spy", "true")
- |> map (apsnd single)
+ val empty = default_default_params |> map (apsnd single)
val extend = I
fun merge data : T = AList.merge (op =) (K true) data
)
@@ -265,7 +262,7 @@
val debug = mode <> Auto_Try andalso lookup_bool "debug"
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
- val spy = lookup_bool "spy"
+ val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
val blocking =
Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
lookup_bool "blocking"