1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -186,10 +186,11 @@
     1.4  
     1.5  val thm_ord = theory_ord o pairself theory_of_thm
     1.6  
     1.7 +val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
     1.8 +
     1.9  fun interesting_terms_types_and_classes ctxt prover term_max_depth
    1.10                                          type_max_depth ts =
    1.11    let
    1.12 -    val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
    1.13      fun is_bad_const (x as (s, _)) args =
    1.14        member (op =) atp_logical_consts s orelse
    1.15        fst (is_built_in_const_for_prover ctxt prover x args)
    1.16 @@ -226,7 +227,7 @@
    1.17           | _ => I)
    1.18          #> fold add_patterns args
    1.19        end
    1.20 -  in [] |> fold add_patterns ts |> sort string_ord end
    1.21 +  in [] |> fold add_patterns ts end
    1.22  
    1.23  fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
    1.24  
    1.25 @@ -249,8 +250,7 @@
    1.26        | Simp => cons "simp"
    1.27        | Def => cons "def")
    1.28  
    1.29 -fun isabelle_dependencies_of all_facts =
    1.30 -  thms_in_proof (SOME all_facts) #> sort string_ord
    1.31 +fun isabelle_dependencies_of all_facts = thms_in_proof (SOME all_facts)
    1.32  
    1.33  val freezeT = Type.legacy_freeze_type
    1.34  
    1.35 @@ -507,18 +507,13 @@
    1.36                     facts =
    1.37    let
    1.38      val timer = Timer.startRealTimer ()
    1.39 -fun check_timer s =
    1.40 -  tracing ("*** " ^ s ^ " " ^ PolyML.makestring (Timer.checkRealTimer timer))
    1.41      val prover = hd provers
    1.42      fun timed_out frac =
    1.43        Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
    1.44 -val _ = check_timer "begin" (*###*)
    1.45      val {fact_graph, ...} = mash_get ctxt
    1.46 -val _ = check_timer " got" (*###*)
    1.47      val new_facts =
    1.48        facts |> filter_out (is_fact_in_graph fact_graph)
    1.49              |> sort (thm_ord o pairself snd)
    1.50 -val _ = check_timer " new facts" (*###*)
    1.51    in
    1.52      if null new_facts then
    1.53        ""
    1.54 @@ -529,7 +524,6 @@
    1.55            ths |> filter_out is_likely_tautology_or_too_meta
    1.56                |> map (rpair () o Thm.get_name_hint)
    1.57                |> Symtab.make
    1.58 -val _ = check_timer " all names" (*###*)
    1.59          fun do_fact _ (accum as (_, true)) = accum
    1.60            | do_fact ((_, (_, status)), th) ((parents, upds), false) =
    1.61              let
    1.62 @@ -539,10 +533,8 @@
    1.63                val upd = (name, parents, feats, deps)
    1.64              in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
    1.65          val parents = parents_wrt_facts ctxt facts fact_graph
    1.66 -val _ = check_timer " parents" (*###*)
    1.67          val ((_, upds), _) =
    1.68            ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
    1.69 -val _ = check_timer " did facts" (*###*)
    1.70          val n = length upds
    1.71          fun trans {thys, fact_graph} =
    1.72            let
    1.73 @@ -550,10 +542,8 @@
    1.74                if Graph.is_empty fact_graph then mash_INIT else mash_ADD
    1.75              val (upds, fact_graph) =
    1.76                ([], fact_graph) |> fold (update_fact_graph ctxt) upds
    1.77 -val _ = check_timer " updated" (*###*)
    1.78            in
    1.79              (mash_INIT_or_ADD ctxt overlord (rev upds);
    1.80 -check_timer " inited/added" (*###*);
    1.81               {thys = thys |> add_thys_for thy,
    1.82                fact_graph = fact_graph})
    1.83            end