1.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Feb 20 10:54:13 2013 +0100
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Feb 20 13:04:03 2013 +0100
     1.3 @@ -112,7 +112,10 @@
     1.4            val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
     1.5            val isar_deps = isar_dependencies_of name_tabs th
     1.6            val facts =
     1.7 -            facts |> filter (fn (_, th') => crude_thm_ord (th', th) = LESS)
     1.8 +            facts
     1.9 +            |> filter (fn (_, th') =>
    1.10 +                          if linearize then crude_thm_ord (th', th) = LESS
    1.11 +                          else thm_less (th', th))
    1.12            val find_suggs =
    1.13              find_suggested_facts ctxt facts #> map fact_of_raw_fact
    1.14            fun get_facts [] compute = compute facts