tuning
authorblanchet
Wed Sep 11 14:07:24 2013 +0200 (2013-09-11 ago)
changeset 5353324ce26e8af12
parent 53532 4ad9599a0847
child 53534 de2027f9aff3
child 53536 69c943125fd3
tuning
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
     1.3 @@ -199,7 +199,7 @@
     1.4    | apply_depth (Abs (_, _, t)) = apply_depth t
     1.5    | apply_depth _ = 0
     1.6  
     1.7 -fun is_too_complex ho_atp t = apply_depth t > max_apply_depth
     1.8 +fun is_too_complex t = apply_depth t > max_apply_depth
     1.9  
    1.10  (* FIXME: Ad hoc list *)
    1.11  val technical_prefixes =
    1.12 @@ -461,7 +461,7 @@
    1.13           fact_count global_facts >= max_facts_for_complex_check then
    1.14          K false
    1.15        else
    1.16 -        is_too_complex ho_atp
    1.17 +        is_too_complex
    1.18      val local_facts = Proof_Context.facts_of ctxt
    1.19      val named_locals = local_facts |> Facts.dest_static []
    1.20      val assms = Assumption.all_assms_of ctxt