# HG changeset patch
# User boehmes
# Date 1251996118 -7200
# Node ID 43d2ac4aa2de8e73df4529a2a86023559ea192c8
# Parent  1b56f8b1e5cc97130becb977d337efff97bd2e56
added option full_typed for sledgehammer action

diff -r 1b56f8b1e5cc -r 43d2ac4aa2de src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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
 
diff -r 1b56f8b1e5cc -r 43d2ac4aa2de src/HOL/Mirabelle/doc/options.txt
--- 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)