# HG changeset patch
# User blanchet
# Date 1378901244 -7200
# Node ID 24ce26e8af1296d3fc0bd585c95dbdcce5621975
# Parent  4ad9599a0847127433867be0d2c7ae87d425476b
tuning

diff -r 4ad9599a0847 -r 24ce26e8af12 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
@@ -199,7 +199,7 @@
   | apply_depth (Abs (_, _, t)) = apply_depth t
   | apply_depth _ = 0
 
-fun is_too_complex ho_atp t = apply_depth t > max_apply_depth
+fun is_too_complex t = apply_depth t > max_apply_depth
 
 (* FIXME: Ad hoc list *)
 val technical_prefixes =
@@ -461,7 +461,7 @@
          fact_count global_facts >= max_facts_for_complex_check then
         K false
       else
-        is_too_complex ho_atp
+        is_too_complex
     val local_facts = Proof_Context.facts_of ctxt
     val named_locals = local_facts |> Facts.dest_static []
     val assms = Assumption.all_assms_of ctxt