Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
honor linearization option also in the evaluation driver
authorblanchet
Wed, 20 Feb 2013 13:04:03 +0100
changeset 51199 e3447c380fe1
parent 51198 4dd63cf5bba5
child 51200 260cb10aac4b
honor linearization option also in the evaluation driver
src/HOL/TPTP/mash_eval.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle