--- 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}
--- 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 @