# HG changeset patch
# User blanchet
# Date 1304330973 -7200
# Node ID aed17803922e71ac50dc09456b1e717023ebcede
# Parent  a7dff503ffabbcc0a67f8718f677877355afc189
tuning

diff -r a7dff503ffab -r aed17803922e src/HOL/ex/tptp_export.ML
--- a/src/HOL/ex/tptp_export.ML	Mon May 02 12:09:33 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Mon May 02 12:09:33 2011 +0200
@@ -40,7 +40,6 @@
 
 fun theorems_mentioned_in_proof_term thm =
   let
-    val PBody {thms, ...} = Thm.proof_body_of thm
     fun collect (s, _, _) = if s <> "" then insert (op =) s else I
     val names =
       [] |> fold_body_thms collect [Thm.proof_body_of thm] |> map fact_name_of
@@ -100,8 +99,6 @@
       |> map_filter (try (fn ((_, loc), (_, th)) =>
              Sledgehammer_ATP_Translate.translate_atp_fact ctxt true
              ((Thm.get_name_hint th, loc), th)))
-    val readable_names = false
-    val explicit_forall = true
     val type_sys =
       ATP_Systems.Preds (ATP_Systems.Polymorphic,
                          if full_types then ATP_Systems.All_Types