# HG changeset patch
# User blanchet
# Date 1307422732 -7200
# Node ID d90151a666cc94b0067d8d2012c33c0fc27d39f9
# Parent  2c88166938eb2dbef040fb721ae4fe5dffba98ce
pass props not thms to ATP translator

diff -r 2c88166938eb -r d90151a666cc src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 23:46:02 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 07 06:58:52 2011 +0200
@@ -130,7 +130,7 @@
   val prepare_atp_problem :
     Proof.context -> format -> formula_kind -> formula_kind -> type_sys
     -> bool option -> bool -> bool -> term list -> term
-    -> ((string * locality) * thm) list
+    -> ((string * locality) * term) list
     -> string problem * string Symtab.table * int * int
        * (string * locality) list vector * int list * int Symtab.table
   val atp_problem_weights : string problem -> (string * real) list
@@ -1386,10 +1386,10 @@
                        facts =
   let
     val thy = Proof_Context.theory_of ctxt
-    val fact_ts = facts |> map (prop_of o snd)
+    val fact_ts = facts |> map snd
     val (facts, fact_names) =
-      facts |> map (fn (name, th) =>
-                        (name, prop_of th)
+      facts |> map (fn (name, t) =>
+                        (name, t)
                         |> make_fact ctxt format type_sys false true true true
                         |> rpair name)
             |> map_filter (try (apfst the))
diff -r 2c88166938eb -r d90151a666cc src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 23:46:02 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 06:58:52 2011 +0200
@@ -155,7 +155,7 @@
   is_metis_prover orf is_smt_prover ctxt orf
   is_atp_installed (Proof_Context.theory_of ctxt)
 
-fun get_slices num_facts slicing slices =
+fun get_slices slicing slices =
   (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
 
 val metis_default_max_relevant = 20
@@ -166,8 +166,7 @@
       metis_default_max_relevant
     else if is_atp thy name then
       fold (Integer.max o fst o snd o snd o snd)
-           (get_slices 16384 (* large number *) slicing
-                       (#best_slices (get_atp thy name) ctxt)) 0
+           (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
     else (* is_smt_prover ctxt name *)
       SMT_Solver.default_max_relevant ctxt name
   end
@@ -579,8 +578,7 @@
           let
             (* If slicing is disabled, we expand the last slice to fill the
                entire time available. *)
-            val actual_slices =
-              get_slices (length facts) slicing (best_slices ctxt)
+            val actual_slices = get_slices slicing (best_slices ctxt)
             val num_actual_slices = length actual_slices
             fun monomorphize_facts facts =
               let
@@ -618,6 +616,7 @@
                            ? filter_out (member (op =) blacklist o fst)
                         |> polymorphism_of_type_sys type_sys <> Polymorphic
                            ? monomorphize_facts
+                        |> map (apsnd prop_of )
                 val real_ms = Real.fromInt o Time.toMilliseconds
                 val slice_timeout =
                   ((real_ms time_left
diff -r 2c88166938eb -r d90151a666cc src/HOL/ex/tptp_export.ML
--- a/src/HOL/ex/tptp_export.ML	Mon Jun 06 23:46:02 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Tue Jun 07 06:58:52 2011 +0200
@@ -101,7 +101,7 @@
     val facts0 = facts_of thy
     val facts =
       facts0 |> map (fn ((_, loc), (_, th)) =>
-                        ((Thm.get_name_hint th, loc), th))
+                        ((Thm.get_name_hint th, loc), prop_of th))
     val explicit_apply = NONE
     val (atp_problem, _, _, _, _, _, _) =
       ATP_Translate.prepare_atp_problem ctxt format