# HG changeset patch
# User blanchet
# Date 1282061894 -7200
# Node ID 78c4988831d1f55a70b8ffce84026eb79eee26fd
# Parent  3b898102963f8ed270a3bd7070c0cf06d2ad6cb5# Parent  dafcd0d19b1138efa135845adc58b6b2d8c708df
merged

diff -r 3b898102963f -r 78c4988831d1 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 17:54:55 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 18:18:14 2010 +0200
@@ -144,7 +144,7 @@
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   max_new_relevant_facts_per_iter = 60 (* FIXME *),
+   max_new_relevant_facts_per_iter = 50 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
 
@@ -198,7 +198,7 @@
       (Unprovable, "Satisfiability detected"),
       (OutOfResources, "Refutation not found"),
       (OldVampire, "not a valid option")],
-   max_new_relevant_facts_per_iter = 50 (* FIXME *),
+   max_new_relevant_facts_per_iter = 45 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
 
diff -r 3b898102963f -r 78c4988831d1 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Aug 17 17:54:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Aug 17 18:18:14 2010 +0200
@@ -267,16 +267,18 @@
         val (x, ty_args) =
           case head of
             CombConst (name as (s, s'), _, ty_args) =>
-            if s = "equal" then
-              (if top_level andalso length args = 2 then name
-               else ("c_fequal", @{const_name fequal}), [])
-            else if top_level then
-              case s of
-                "c_False" => (("$false", s'), [])
-              | "c_True" => (("$true", s'), [])
-              | _ => (name, if full_types then [] else ty_args)
-            else
-              (name, if full_types then [] else ty_args)
+            let val ty_args = if full_types then [] else ty_args in
+              if s = "equal" then
+                if top_level andalso length args = 2 then (name, [])
+                else (("c_fequal", @{const_name fequal}), ty_args)
+              else if top_level then
+                case s of
+                  "c_False" => (("$false", s'), [])
+                | "c_True" => (("$true", s'), [])
+                | _ => (name, ty_args)
+              else
+                (name, ty_args)
+            end
           | CombVar (name, _) => (name, [])
           | CombApp _ => raise Fail "impossible \"CombApp\""
         val t = ATerm (x, map fo_term_for_combtyp ty_args @