# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 8005fc9b65ec5bea844925fc469c6238bd854d0c
# Parent  1d375de437e90d33b929a51a933a23f763180fcf
ensure that Auto Sledgehammer is run with full type information

diff -r 1d375de437e9 -r 8005fc9b65ec doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 15:29:19 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 15:29:19 2011 +0200
@@ -354,12 +354,13 @@
 You can instruct Sledgehammer to run automatically on newly entered theorems by
 enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
 General. For automatic runs, only the first prover set using \textit{provers}
-(\S\ref{mode-of-operation}) is considered, \textit{verbose}
-(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled,
-fewer facts are passed to the prover, \textit{slicing}
-(\S\ref{mode-of-operation}) is disabled, and \textit{timeout}
+(\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
+\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{timeout}
 (\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in
-Proof General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
+Proof General's ``Isabelle'' menu, \textit{full\_types}
+(\S\ref{problem-encoding}) is enabled, and \textit{verbose}
+(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled.
+Sledgehammer's output is also more concise.
 
 \section{Option Reference}
 \label{option-reference}
@@ -555,17 +556,10 @@
 
 \opfalse{full\_types}{partial\_types}
 Specifies whether full type information is encoded in ATP problems. Enabling
-this option prevents the discovery of type-incorrect proofs, but it also tends
-to slow down the ATPs significantly. For historical reasons, the default value
-of this option can be overridden using the option ``Sledgehammer: Full Types''
-from the ``Isabelle'' menu in Proof General.
-
-\opfalse{full\_types}{partial\_types}
-Specifies whether full-type information is encoded in ATP problems. Enabling
-this option can prevent the discovery of type-incorrect proofs, but it also
-tends to slow down the ATPs significantly. For historical reasons, the default
-value of this option can be overridden using the option ``Sledgehammer: Full
-Types'' from the ``Isabelle'' menu in Proof General.
+this option prevents the discovery of type-incorrect proofs, but it can slow
+down the ATP slightly. This option is implicitly enabled for automatic runs. For
+historical reasons, the default value of this option can be overridden using the
+option ``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General.
 
 \opdefault{type\_sys}{string}{smart}
 Specifies the type system to use in ATP problems. The option can take the
diff -r 1d375de437e9 -r 8005fc9b65ec src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:19 2011 +0200
@@ -241,7 +241,9 @@
     val provers = lookup_string "provers" |> space_explode " "
                   |> auto ? single o hd
     val type_sys =
-      case lookup_string "type_sys" of
+      if auto then
+        Smart_Type_Sys true
+      else case lookup_string "type_sys" of
         "smart" => Smart_Type_Sys (lookup_bool "full_types")
       | s => Dumb_Type_Sys (type_sys_from_string s)
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"