--- 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