--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 03 17:55:31 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 03 18:41:58 2009 +0200
@@ -28,6 +28,7 @@
val proverK = "prover"
val keepK = "keep"
val metisK = "metis"
+val full_typesK = "full_types"
local
@@ -102,7 +103,9 @@
run_sledgehammer (args, pre, timeout, log)
|> run_metis (args, pre, timeout, log)
-fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
+fun invoke args =
+ let val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
+ in Mirabelle.register ("sledgehammer", sledgehammer_action args) end
end
--- a/src/HOL/Mirabelle/doc/options.txt Thu Sep 03 17:55:31 2009 +0200
+++ b/src/HOL/Mirabelle/doc/options.txt Thu Sep 03 18:41:58 2009 +0200
@@ -4,3 +4,4 @@
* keep=PATH: path where to keep temporary files created by sledgehammer
* metis=X: apply metis with the theorems found by sledgehammer (X may be any
non-empty string)
+ * full_types=X: turn on full-typed encoding (X may be any non-empty string)