--- 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)