src/HOL/ex/atp_export.ML
changeset 43245 cef69d31bfa4
parent 43224 97906dfd39b7
child 43259 30c141dc22d6
--- a/src/HOL/ex/atp_export.ML	Tue Jun 07 14:06:12 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Tue Jun 07 14:17:35 2011 +0200
@@ -65,7 +65,7 @@
           commas (map (prefix ATP_Translate.const_prefix o ascii_of)
                       (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
       in File.append path s end
-    val thms = facts_of thy |> map (snd o snd)
+    val thms = facts_of thy |> map snd
     val _ = map do_thm thms
   in () end
 
@@ -100,7 +100,7 @@
     val _ = File.write path ""
     val facts0 = facts_of thy
     val facts =
-      facts0 |> map (fn ((_, loc), (_, th)) =>
+      facts0 |> map (fn ((_, loc), th) =>
                         ((Thm.get_name_hint th, loc), prop_of th))
     val explicit_apply = NONE
     val (atp_problem, _, _, _, _, _, _) =
@@ -108,7 +108,7 @@
           ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
           [] @{prop False} facts
     val infers =
-      facts0 |> map (fn (_, (_, th)) =>
+      facts0 |> map (fn (_, th) =>
                         (fact_name_of (Thm.get_name_hint th),
                          theorems_mentioned_in_proof_term th))
     val infers =