# HG changeset patch # User blanchet # Date 1304335787 -7200 # Node ID c8673078f9153a3eacec4e183e10464723eea389 # Parent 0c76cf4838998a78a2b72337d66b2bed6d1636e8 fix ROOT.ML and handle "readable_names" reference slightly more cleanly diff -r 0c76cf483899 -r c8673078f915 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Mon May 02 12:09:33 2011 +0200 +++ b/src/HOL/ex/ROOT.ML Mon May 02 13:29:47 2011 +0200 @@ -11,7 +11,8 @@ "Normalization_by_Evaluation", "Hebrew", "Chinese", - "Serbian" + "Serbian", + "TPTP_Export" ]; use_thys [ @@ -78,7 +79,7 @@ ]; Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs) - use_thy "CASC_THF0"; + use_thy "CASC_Setup"; if getenv "ISABELLE_GHC" = "" then () else use_thy "Quickcheck_Narrowing_Examples"; diff -r 0c76cf483899 -r c8673078f915 src/HOL/ex/TPTP_Export.thy --- a/src/HOL/ex/TPTP_Export.thy Mon May 02 12:09:33 2011 +0200 +++ b/src/HOL/ex/TPTP_Export.thy Mon May 02 13:29:47 2011 +0200 @@ -4,10 +4,16 @@ begin ML {* +val readable_names = !Sledgehammer_ATP_Translate.readable_names; +Sledgehammer_ATP_Translate.readable_names := false +*} + +ML {* val thy = @{theory Complex_Main} val ctxt = @{context} *} +(* ML {* TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true "/tmp/infs_full_types.tptp" @@ -22,5 +28,10 @@ TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy "/tmp/graph.out" *} +*) + +ML {* +Sledgehammer_ATP_Translate.readable_names := readable_names +*} end diff -r 0c76cf483899 -r c8673078f915 src/HOL/ex/tptp_export.ML --- 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 13:29:47 2011 +0200 @@ -17,8 +17,6 @@ structure TPTP_Export : TPTP_EXPORT = struct -val _ = Sledgehammer_ATP_Translate.readable_names := false - val ascii_of = Metis_Translate.ascii_of val fact_name_of = prefix Sledgehammer_ATP_Translate.fact_prefix o ascii_of