--- a/src/HOL/TPTP/mash_export.ML Fri Aug 03 17:56:35 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Aug 03 17:56:35 2012 +0200
@@ -37,10 +37,10 @@
fun has_thy thy th =
Context.theory_name thy = Context.theory_name (theory_of_thm th)
-fun all_non_technical_facts ctxt thy =
+fun all_facts ctxt thy =
let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
- all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
- |> filter_out (is_thm_technical o snd)
+ nearly_all_facts (Proof_Context.init_global thy) false no_fact_override
+ Symtab.empty css [] [] @{prop True}
end
fun parent_facts thy thy_map =
@@ -67,7 +67,7 @@
val _ = File.append path s
in [fact] end
val thy_map =
- all_non_technical_facts ctxt thy
+ all_facts ctxt thy
|> not include_thy ? filter_out (has_thy thy o snd)
|> thy_map_from_facts
fun do_thy facts =
@@ -82,7 +82,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val facts =
- all_non_technical_facts ctxt thy
+ all_facts ctxt thy
|> not include_thy ? filter_out (has_thy thy o snd)
fun do_fact ((_, stature), th) =
let
@@ -98,7 +98,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val ths =
- all_non_technical_facts ctxt thy
+ all_facts ctxt thy
|> not include_thy ? filter_out (has_thy thy o snd)
|> map snd
val all_names = all_names ths
@@ -117,7 +117,7 @@
val _ = File.write path ""
val prover = hd provers
val facts =
- all_non_technical_facts ctxt thy
+ all_facts ctxt thy
|> not include_thy ? filter_out (has_thy thy o snd)
val ths = facts |> map snd
val all_names = all_names ths
@@ -136,7 +136,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
- val facts = all_non_technical_facts ctxt thy
+ val facts = all_facts ctxt thy
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
@@ -167,7 +167,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
- val facts = all_non_technical_facts ctxt thy
+ val facts = all_facts ctxt thy
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Aug 03 17:56:35 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Aug 03 17:56:35 2012 +0200
@@ -182,14 +182,17 @@
apply_depth t > max_apply_depth orelse
(not ho_atp andalso formula_has_too_many_lambdas [] t)
-(* These theories contain auxiliary facts that could positively confuse
- Sledgehammer if they were included. *)
-val sledgehammer_prefixes =
- ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
+(* FIXME: Ad hoc list *)
+val technical_prefixes =
+ ["ATP", "Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Meson",
+ "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", "Quickcheck",
+ "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence",
+ "Sledgehammer", "SMT"]
+ |> map (suffix Long_Name.separator)
-val exists_sledgehammer_const =
- exists_Const (fn (s, _) =>
- exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)
+fun has_technical_prefix s =
+ exists (fn pref => String.isPrefix pref s) technical_prefixes
+val exists_technical_const = exists_Const (has_technical_prefix o fst)
(* FIXME: make more reliable *)
val exists_low_level_class_const =
@@ -224,9 +227,8 @@
is_likely_tautology_or_too_meta th orelse
let val t = prop_of th in
is_formula_too_complex ho_atp t orelse
- exists_type type_has_top_sort t orelse
- exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
- is_that_fact th
+ exists_type type_has_top_sort t orelse exists_technical_const t orelse
+ exists_low_level_class_const t orelse is_that_fact th
end
fun hackish_string_for_term thy t =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 03 17:56:35 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 03 17:56:35 2012 +0200
@@ -45,7 +45,6 @@
val atp_dependencies_of :
Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
-> thm -> bool * string list option
- val is_thm_technical : thm -> bool
val mash_CLEAR : Proof.context -> unit
val mash_ADD :
Proof.context -> bool
@@ -402,14 +401,6 @@
| _ => (false, isar_deps)
end
-val technical_theories =
- ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
- "New_DSequence", "New_Random_Sequence", "Quickcheck",
- "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
-
-val is_thm_technical =
- member (op =) technical_theories o Context.theory_name o theory_of_thm
-
(*** Low-level communication with MaSh ***)
@@ -727,8 +718,7 @@
Time.+ (Timer.checkRealTimer timer, commit_timeout)
val {fact_G} = mash_get ctxt
val (old_facts, new_facts) =
- facts |> filter_out (is_thm_technical o snd)
- |> List.partition (is_fact_in_graph fact_G)
+ facts |> List.partition (is_fact_in_graph fact_G)
||> sort (thm_ord o pairself snd)
in
if null new_facts andalso (not atp orelse null old_facts) then