renamed "const_args" option value to "args"

--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Apr 05 10:54:09 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Apr 05 11:39:48 2011 +0200
@@ -564,21 +564,20 @@
 \item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
 its type.
 
+\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with
+their type parameters, which are passed as extra arguments. This value is
+ignored if \textit{full\_types} is enabled.
+
 \item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names.
 This value is available only if \textit{monomorphize} is enabled and
 \textit{full\_types} is disabled.
 
-\item[$\bullet$] \textbf{\textit{const\_args}:} Constants are annotated with
-their type parameters, which are passed as extra arguments. This value is
-ignored if \textit{full\_types} is enabled.
-
 \item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
 ATP. This value is ignored if \textit{full\_types} is enabled.
 
-\item[$\bullet$] \textbf{\textit{smart}:} This is the same as
-\textit{tags} if \textit{full\_types} is enabled; otherwise, this is the
-same as \textit{mangled} if \textit{monomorphize} is enabled and
-\textit{const\_args} otherwise.
+\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
+this is the same as \textit{tags}; otherwise, this is the
+same as \textit{args} otherwise.
 \end{enum}
 
 For SMT solvers, the type system is always \textit{mangled}.

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Apr 05 10:54:09 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Apr 05 11:39:48 2011 +0200
@@ -14,7 +14,7 @@
 
   datatype type_system =
     Tags of bool |
-    Const_Args |
+    Args |
     Mangled |
     No_Types
 
@@ -63,7 +63,7 @@
 
 datatype type_system =
   Tags of bool |
-  Const_Args |
+  Args |
   Mangled |
   No_Types
 
@@ -83,7 +83,7 @@
 fun needs_type_args thy type_sys s =
   case type_sys of
     Tags full_types => not full_types andalso is_overloaded thy s
-  | Const_Args => is_overloaded thy s
+  | Args => is_overloaded thy s
   | Mangled => true
   | No_Types => false
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 05 10:54:09 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 05 11:39:48 2011 +0200
@@ -240,15 +240,13 @@
     val type_sys =
       case (lookup_string "type_sys", lookup_bool "full_types") of
         ("tags", full_types) => Tags full_types
-      | ("const_args", false) => Const_Args
-      | ("mangled", false) => if monomorphize then Mangled else Const_Args
+      | ("args", false) => Args
+      | ("mangled", false) => if monomorphize then Mangled else Args
       | ("none", false) => No_Types
       | (type_sys, full_types) =>
-        if member (op =) ["const_args", "mangled", "none", "smart"]
+        if member (op =) ["args", "mangled", "none", "smart"]
                   type_sys then
-          if full_types then Tags true
-          else if monomorphize then Mangled
-          else Const_Args
+          if full_types then Tags true else Args
         else
           error ("Unknown type system: " ^ quote type_sys ^ ".")
     val explicit_apply = lookup_bool "explicit_apply"