--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 25 17:13:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 25 17:26:14 2010 +0200
@@ -68,7 +68,6 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("respect_no_atp", "true"),
("relevance_threshold", "50"),
("relevance_convergence", "320"),
("theory_relevant", "smart"),
@@ -85,7 +84,6 @@
("no_overlord", "overlord"),
("partial_types", "full_types"),
("implicit_apply", "explicit_apply"),
- ("ignore_no_atp", "respect_no_atp"),
("theory_irrelevant", "theory_relevant"),
("defs_irrelevant", "defs_relevant"),
("no_isar_proof", "isar_proof")]
@@ -167,7 +165,6 @@
val atps = lookup_string "atps" |> space_explode " "
val full_types = lookup_bool "full_types"
val explicit_apply = lookup_bool "explicit_apply"
- val respect_no_atp = lookup_bool "respect_no_atp"
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val relevance_convergence =
@@ -181,7 +178,7 @@
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
+ relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
theory_relevant = theory_relevant, defs_relevant = defs_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,