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