# HG changeset patch
# User blanchet
# Date 1361361843 -3600
# Node ID e3447c380fe19604ac27c0ce03a527d17f987224
# Parent  4dd63cf5bba542ae157c17053179e45b2acd45a4
honor linearization option also in the evaluation driver

diff -r 4dd63cf5bba5 -r e3447c380fe1 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Wed Feb 20 10:54:13 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Feb 20 13:04:03 2013 +0100
@@ -112,7 +112,10 @@
           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
           val isar_deps = isar_dependencies_of name_tabs th
           val facts =
-            facts |> filter (fn (_, th') => crude_thm_ord (th', th) = LESS)
+            facts
+            |> filter (fn (_, th') =>
+                          if linearize then crude_thm_ord (th', th) = LESS
+                          else thm_less (th', th))
           val find_suggs =
             find_suggested_facts ctxt facts #> map fact_of_raw_fact
           fun get_facts [] compute = compute facts