got rid of 'linearize' option

--- a/src/HOL/TPTP/MaSh_Export.thy	Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Fri May 30 12:27:51 2014 +0200
@@ -34,7 +34,6 @@
 val prover = hd provers
 val range = (1, (* ### NONE *) SOME 100)
 val step = 1
-val linearize = false
 val max_suggestions = 1024
 val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
@@ -47,21 +46,21 @@
   ()
 *}
 
-ML {* Options.put_default @{system_option MaSh} "sml_knn" *}
+ML {* Options.put_default @{system_option MaSh} "sml_nb" *}
 
 ML {*
 if do_it then
-  generate_mash_suggestions @{context} params (range, step) thys linearize max_suggestions
+  generate_mash_suggestions @{context} params (range, step) thys max_suggestions
     (prefix ^ "mash_sml_knn_suggestions")
 else
   ()
 *}
 
-ML {* Options.put_default @{system_option MaSh} "sml_nb" *}
+ML {* Options.put_default @{system_option MaSh} "sml_knn" *}
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
+  generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
     (prefix ^ "mash_sml_nb_suggestions")
 else
   ()
@@ -71,7 +70,7 @@
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
+  generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
     (prefix ^ "mepo_suggestions")
 else
   ()
@@ -79,7 +78,7 @@
 
 ML {*
 if do_it then
-  generate_accessibility @{context} thys linearize (prefix ^ "mash_accessibility")
+  generate_accessibility @{context} thys (prefix ^ "mash_accessibility")
 else
   ()
 *}
@@ -93,14 +92,14 @@
 
 ML {*
 if do_it then
-  generate_isar_dependencies @{context} range thys linearize (prefix ^ "mash_dependencies")
+  generate_isar_dependencies @{context} range thys (prefix ^ "mash_dependencies")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_isar_commands @{context} prover (range, step) thys linearize max_suggestions
+  generate_isar_commands @{context} prover (range, step) thys max_suggestions
     (prefix ^ "mash_commands")
 else
   ()
@@ -108,7 +107,7 @@
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
+  generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
     (prefix ^ "mepo_suggestions")
 else
   ()
@@ -124,15 +123,14 @@
 
 ML {*
 if do_it then
-  generate_prover_dependencies @{context} params range thys linearize
-    (prefix ^ "mash_prover_dependencies")
+  generate_prover_dependencies @{context} params range thys (prefix ^ "mash_prover_dependencies")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_prover_commands @{context} params (range, step) thys linearize max_suggestions
+  generate_prover_commands @{context} params (range, step) thys max_suggestions
     (prefix ^ "mash_prover_commands")
 else
   ()

--- a/src/HOL/TPTP/mash_export.ML	Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri May 30 12:27:51 2014 +0200
@@ -9,20 +9,20 @@
 sig
   type params = Sledgehammer_Prover.params
 
-  val generate_accessibility : Proof.context -> theory list -> bool -> string -> unit
+  val generate_accessibility : Proof.context -> theory list -> string -> unit
   val generate_features : Proof.context -> theory list -> string -> unit
-  val generate_isar_dependencies : Proof.context -> int * int option -> theory list -> bool ->
+  val generate_isar_dependencies : Proof.context -> int * int option -> theory list -> string ->
+    unit
+  val generate_prover_dependencies : Proof.context -> params -> int * int option -> theory list ->
     string -> unit
-  val generate_prover_dependencies : Proof.context -> params -> int * int option -> theory list ->
-    bool -> string -> unit
   val generate_isar_commands : Proof.context -> string -> (int * int option) * int -> theory list ->
-    bool -> int -> string -> unit
+    int -> string -> unit
   val generate_prover_commands : Proof.context -> params -> (int * int option) * int ->
-    theory list -> bool -> int -> string -> unit
+    theory list -> int -> string -> unit
   val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int ->
-    theory list -> bool -> int -> string -> unit
+    theory list -> int -> string -> unit
   val generate_mash_suggestions : Proof.context -> params -> (int * int option) * int ->
-    theory list -> bool -> int -> string -> unit
+    theory list -> int -> string -> unit
   val generate_mesh_suggestions : int -> string -> string -> string -> unit
 end;
 
@@ -50,14 +50,13 @@
 
 fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th))
 
-fun generate_accessibility ctxt thys linearize file_name =
+fun generate_accessibility ctxt thys file_name =
   let
-    val path = file_name |> Path.explode
+    val path = Path.explode file_name
     val _ = File.write path ""
 
     fun do_fact (parents, fact) prevs =
       let
-        val parents = if linearize then prevs else parents
         val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n"
         val _ = File.append path s
       in [fact] end
@@ -113,10 +112,10 @@
     | 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 file_name =
   let
-    val path = file_name |> Path.explode
-    val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
+    val path = Path.explode file_name
+    val facts = filter_out (has_thys thys o snd) (all_facts ctxt)
     val name_tabs = build_name_tables nickname_of_thm facts
 
     fun do_fact (j, (_, th)) =
@@ -124,11 +123,11 @@
         let
           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
-          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
+          val access_facts = filter_accessible_from th facts
+          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
       else
         ""
 
@@ -149,8 +148,7 @@
   null isar_deps orelse
   is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
 
-fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys linearize max_suggs
-    file_name =
+fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
   let
     val ho_atp = is_ho_atp ctxt prover
     val path = file_name |> Path.explode
@@ -168,13 +166,10 @@
           val goal_feats =
             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
+          val access_facts = filter_accessible_from th new_facts @ old_facts
           val (marker, deps) =
-            smart_dependencies_of ctxt params_opt access_facts name_tabs th
-                                  (SOME isar_deps)
-          val parents = if linearize then prevs else parents
+            smart_dependencies_of ctxt params_opt access_facts name_tabs th (SOME isar_deps)
+          val parents = parents
           fun extra_features_of (((_, stature), th), weight) =
             [prop_of th]
             |> features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature
@@ -223,7 +218,7 @@
   generate_isar_or_prover_commands ctxt prover (SOME params)
 
 fun generate_mepo_or_mash_suggestions mepo_or_mash_suggested_facts ctxt
-    (params as {provers = prover :: _, ...}) (range, step) thys linearize max_suggs file_name =
+    (params as {provers = prover :: _, ...}) (range, step) thys max_suggs file_name =
   let
     val ho_atp = is_ho_atp ctxt prover
     val path = file_name |> Path.explode
@@ -246,7 +241,7 @@
             let
               val suggs =
                 old_facts
-                |> not linearize ? filter_accessible_from th
+                |> filter_accessible_from th
                 |> mepo_or_mash_suggested_facts ctxt params max_suggs hyp_ts concl_t
                 |> map (nickname_of_thm o snd)
             in