# HG changeset patch
# User blanchet
# Date 1344009395 -7200
# Node ID ac58317ef11f2fe01b13c21de74b9853cb3a8fbb
# Parent  0ba2e9be9f2053da8ac169b43dd7b38fe873cc15
rule out same "technical" theories for MePo as for MaSh

diff -r 0ba2e9be9f20 -r ac58317ef11f src/HOL/TPTP/mash_export.ML
--- 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)
diff -r 0ba2e9be9f20 -r ac58317ef11f src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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 =
diff -r 0ba2e9be9f20 -r ac58317ef11f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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