Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
compile + fixed naming convention
authorblanchet
Tue, 09 Apr 2013 15:19:14 +0200
changeset 51649 5d882158c221
parent 51648 3e09226c3378
child 51650 3dd495cd98a2
compile + fixed naming convention
src/HOL/TPTP/atp_theory_export.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle