# HG changeset patch
# User blanchet
# Date 1400847141 -7200
# Node ID 5bc908e5bf42d8ea6d1f6d4224bc08e56fb5c8bc
# Parent  3d4b172d22090dcdb334e539562d05619ae36741
fixed semantics of 'linearize'

diff -r 3d4b172d2209 -r 5bc908e5bf42 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri May 23 14:12:20 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri May 23 14:12:21 2014 +0200
@@ -111,8 +111,7 @@
     | NONE => (omitted_marker, []))
   end
 
-fun generate_isar_or_prover_dependencies ctxt params_opt range thys linearize
-                                         file_name =
+fun generate_isar_or_prover_dependencies ctxt params_opt range thys linearize file_name =
   let
     val path = file_name |> Path.explode
     val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
@@ -124,8 +123,7 @@
           val name = nickname_of_thm th
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
           val access_facts =
-            if linearize then take (j - 1) facts
-            else facts |> filter_accessible_from th
+            if linearize then take (j - 1) facts else facts |> filter_accessible_from th
           val (marker, deps) =
             smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE
         in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end
@@ -169,8 +167,8 @@
             features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature [prop_of th]
             |> sort_wrt fst
           val access_facts =
-            (if linearize then take (j - 1) new_facts
-             else new_facts |> filter_accessible_from th) @ old_facts
+            (if linearize then take (j - 1) new_facts else new_facts |> filter_accessible_from th) @
+            old_facts
           val (marker, deps) =
             smart_dependencies_of ctxt params_opt access_facts name_tabs th
                                   (SOME isar_deps)
@@ -246,7 +244,7 @@
             let
               val suggs =
                 old_facts
-                |> linearize ? filter_accessible_from th
+                |> not linearize ? filter_accessible_from th
                 |> Sledgehammer_Fact.drop_duplicate_facts
                 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t
                 |> map (nickname_of_thm o snd)