# HG changeset patch
# User blanchet
# Date 1365513554 -7200
# Node ID 5d882158c2212ab9426174823f14a23d53eb1b7d
# Parent  3e09226c33782d8978be5c7426a9208d009d1109
compile + fixed naming convention

diff -r 3e09226c3378 -r 5d882158c221 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Tue Apr 09 15:19:14 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Tue Apr 09 15:19:14 2013 +0200
@@ -68,9 +68,9 @@
       handle TimeLimit.TimeOut => SOME TimedOut
     val _ =
       tracing ("Ran ATP: " ^
-               case outcome of
-                 NONE => "Success"
-               | SOME failure => string_for_failure failure)
+               (case outcome of
+                  NONE => "Success"
+                | SOME failure => string_for_failure failure))
   in outcome end
 
 fun is_problem_line_reprovable ctxt format prelude axioms deps
@@ -269,7 +269,8 @@
 
 (* Convention: theoryname__goalname *)
 fun problem_name_of base_name alt =
-  base_name ^ "_" ^ perhaps (try (unprefix base_name)) alt ^ problem_suffix
+  base_name ^ "__" ^ perhaps (try (unprefix (base_name ^ "_"))) alt ^
+  problem_suffix
 
 fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc
                                            dir_name =