# HG changeset patch
# User blanchet
# Date 1360916240 -3600
# Node ID e32114b255511139431473aa696816a66132e054
# Parent  d03ded5dcf65c3994a8f369c0af4b7fbb0043d62
tuned code

diff -r d03ded5dcf65 -r e32114b25551 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Fri Feb 15 09:17:20 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Feb 15 09:17:20 2013 +0100
@@ -110,7 +110,8 @@
           val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
           val isar_deps = isar_dependencies_of name_tabs th
-          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+          val facts =
+            facts |> filter (fn (_, th') => crude_thm_ord (th', th) = LESS)
           val find_suggs =
             find_suggested_facts ctxt facts #> map fact_of_raw_fact
           fun get_facts [] compute = compute facts
diff -r d03ded5dcf65 -r e32114b25551 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Feb 15 09:17:20 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Fri Feb 15 09:17:20 2013 +0100
@@ -48,7 +48,7 @@
 fun all_facts ctxt =
   let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
     Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css
-    |> sort (thm_ord o pairself snd)
+    |> sort (crude_thm_ord o pairself snd)
   end
 
 fun generate_accessibility ctxt thys include_thys file_name =
diff -r d03ded5dcf65 -r e32114b25551 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 15 09:17:20 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 15 09:17:20 2013 +0100
@@ -55,8 +55,7 @@
   val mesh_facts :
     ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
     -> 'a list
-  val theory_ord : theory * theory -> order
-  val thm_ord : thm * thm -> order
+  val crude_thm_ord : thm * thm -> order
   val goal_of_thm : theory -> thm -> thm
   val run_prover_for_mash :
     Proof.context -> params -> string -> fact list -> thm -> prover_result
@@ -510,7 +509,7 @@
 val lams_feature = ("lams", 2.0 (* FUDGE *))
 val skos_feature = ("skos", 2.0 (* FUDGE *))
 
-fun theory_ord p =
+fun crude_theory_ord p =
   if Theory.subthy p then
     if Theory.eq_thy p then EQUAL else LESS
   else if Theory.subthy (swap p) then
@@ -519,8 +518,8 @@
     EQUAL => string_ord (pairself Context.theory_name p)
   | order => order
 
-fun thm_ord p =
-  case theory_ord (pairself theory_of_thm p) of
+fun crude_thm_ord p =
+  case crude_theory_ord (pairself theory_of_thm p) of
     EQUAL =>
     let val q = pairself nickname_of_thm p in
       (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
@@ -697,7 +696,8 @@
       val thy = Proof_Context.theory_of ctxt
       val goal = goal_of_thm thy th
       val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
-      val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+      val facts =
+        facts |> filter (fn (_, th') => crude_thm_ord (th', th) = LESS)
       fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
       fun is_dep dep (_, th) = nickname_of_thm th = dep
       fun add_isar_dep facts dep accum =
@@ -801,7 +801,7 @@
       val unknown_chained =
         inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown
       val proximity =
-        facts |> sort (thm_ord o pairself snd o swap)
+        facts |> sort (crude_thm_ord o pairself snd o swap)
               |> take max_proximity_facts
       val mess =
         [(0.90 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
@@ -904,7 +904,7 @@
     fun next_commit_time () =
       Time.+ (Timer.checkRealTimer timer, commit_timeout)
     val {access_G, ...} = peek_state ctxt I
-    val facts = facts |> sort (thm_ord o pairself snd)
+    val facts = facts |> sort (crude_thm_ord o pairself snd)
     val (old_facts, new_facts) =
       facts |> List.partition (is_fact_in_graph access_G snd)
   in
@@ -996,7 +996,7 @@
               (* crude approximation *)
               val ancestors =
                 old_facts
-                |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER)
+                |> filter (fn (_, th) => crude_thm_ord (th, last_th) <> GREATER)
               val parents = maximal_in_graph access_G ancestors
               val (learns, (_, n, _, _)) =
                 ([], (parents, 0, next_commit_time (), false))