# HG changeset patch
# User blanchet
# Date 1291843072 -3600
# Node ID b98fe4de1ecdb25cd49524ab58425c7b4f4854be
# Parent  2e69fb6331cbba51cc18f9e7b015537e1b30ecaa
renamings

diff -r 2e69fb6331cb -r b98fe4de1ecd src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 08 22:17:52 2010 +0100
@@ -370,7 +370,7 @@
     val problem =
       {state = st', goal = goal, subgoal = i,
        subgoal_count = Sledgehammer_Util.subgoal_count st,
-       facts = facts |> map Sledgehammer_Provers.Untranslated}
+       facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
     val time_limit =
       (case hard_timeout of
         NONE => I
diff -r 2e69fb6331cb -r b98fe4de1ecd src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Wed Dec 08 22:17:52 2010 +0100
@@ -43,8 +43,8 @@
                                       not (String.isSubstring "HOL" s))
                         (prop_of goal))
     val problem =
-      {state = Proof.init ctxt, goal = goal, subgoal = i,
-       subgoal_count = n, facts = map Sledgehammer_Provers.Untranslated facts}
+      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
+       facts = map Sledgehammer_Provers.Untranslated_Fact facts}
   in
     (case prover params (K "") problem of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
diff -r 2e69fb6331cb -r b98fe4de1ecd src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Dec 08 22:17:52 2010 +0100
@@ -55,7 +55,7 @@
        max_relevant = NONE, isar_proof = isar_proof,
        isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
     val facts =
-      facts |> maps (fn (n, ths) => ths |> map (Untranslated o pair n))
+      facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     val {goal, ...} = Proof.goal state
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
diff -r 2e69fb6331cb -r b98fe4de1ecd src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 08 22:17:52 2010 +0100
@@ -29,16 +29,17 @@
      timeout: Time.time,
      expect: string}
 
-  datatype fact =
-    Untranslated of (string * locality) * thm |
-    ATP_Translated of term * ((string * locality) * translated_formula) option
+  datatype prover_fact =
+    Untranslated_Fact of (string * locality) * thm |
+    ATP_Translated_Fact of
+      term * ((string * locality) * translated_formula) option
 
   type prover_problem =
     {state: Proof.state,
      goal: thm,
      subgoal: int,
      subgoal_count: int,
-     facts: fact list}
+     facts: prover_fact list}
 
   type prover_result =
     {outcome: failure option,
@@ -210,16 +211,17 @@
    timeout: Time.time,
    expect: string}
 
-datatype fact =
-  Untranslated of (string * locality) * thm |
-  ATP_Translated of term * ((string * locality) * translated_formula) option
+datatype prover_fact =
+  Untranslated_Fact of (string * locality) * thm |
+  ATP_Translated_Fact of
+    term * ((string * locality) * translated_formula) option
 
 type prover_problem =
   {state: Proof.state,
    goal: thm,
    subgoal: int,
    subgoal_count: int,
-   facts: fact list}
+   facts: prover_fact list}
 
 type prover_result =
   {outcome: failure option,
@@ -252,10 +254,11 @@
 
 (* generic TPTP-based ATPs *)
 
-fun dest_Untranslated (Untranslated p) = p
-  | dest_Untranslated (ATP_Translated _) = raise Fail "dest_Untranslated"
-fun atp_translated_fact ctxt (Untranslated p) = translate_atp_fact ctxt p
-  | atp_translated_fact _ (ATP_Translated p) = p
+fun dest_Untranslated_Fact (Untranslated_Fact p) = p
+  | dest_Untranslated_Fact (ATP_Translated_Fact _) =
+    raise Fail "dest_Untranslated_Fact"
+fun atp_translated_fact ctxt (Untranslated_Fact p) = translate_atp_fact ctxt p
+  | atp_translated_fact _ (ATP_Translated_Fact p) = p
 
 fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
   | int_opt_add _ _ = NONE
@@ -527,7 +530,8 @@
       #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
     val state = state |> Proof.map_context repair_context
     val thy = Proof.theory_of state
-    val get_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
+    val get_fact =
+      Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated_Fact
     val facts = facts |> map_filter get_fact
     val {outcome, used_facts, run_time_in_msecs} =
       smt_filter_loop params remote state subgoal facts
diff -r 2e69fb6331cb -r b98fe4de1ecd src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 08 22:17:52 2010 +0100
@@ -101,8 +101,8 @@
 (* FUDGE *)
 val auto_max_relevant_divisor = 2
 
-fun fact_name (Untranslated ((name, _), _)) = SOME name
-  | fact_name (ATP_Translated (_, p)) = Option.map (fst o fst) p
+fun fact_name (Untranslated_Fact ((name, _), _)) = SOME name
+  | fact_name (ATP_Translated_Fact (_, p)) = Option.map (fst o fst) p
 
 fun run_sledgehammer (params as {blocking, debug, provers, full_types,
                                  relevance_thresholds, max_relevant, ...})
@@ -171,9 +171,9 @@
           end
       val run_atps =
         run_provers "ATP" full_types atp_relevance_fudge
-                    (ATP_Translated o translate_atp_fact ctxt) atps
+                    (ATP_Translated_Fact o translate_atp_fact ctxt) atps
       val run_smts =
-        run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
+        run_provers "SMT solver" true smt_relevance_fudge Untranslated_Fact smts
       fun run_atps_and_smt_solvers () =
         [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
     in