# HG changeset patch
# User blanchet
# Date 1341956163 -7200
# Node ID 288effe53e19c45b7f260f5d75a4ded81aab2ceb
# Parent  f2dd90cc724b6edc06120ee8e86b1968a4fbb126
generate theory name as a feature

diff -r f2dd90cc724b -r 288effe53e19 src/HOL/TPTP/ATP_Theory_Export.thy
--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Jul 10 18:41:34 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Jul 10 23:36:03 2012 +0200
@@ -15,8 +15,8 @@
 *}
 
 ML {*
-val do_it = false; (* switch to "true" to generate the files *)
-val thy = @{theory Complex_Main};
+val do_it = true (* ### *); (* switch to "true" to generate the files *)
+val thy = @{theory Nat};
 val ctxt = @{context}
 *}
 
@@ -33,16 +33,16 @@
 
 ML {*
 if do_it then
-  "/tmp/mash_accessibility.out"
-  |> generate_mash_accessibility_file_for_theory thy false
+  "/tmp/mash_features.out"
+  |> generate_mash_feature_file_for_theory thy false
 else
   ()
 *}
 
 ML {*
 if do_it then
-  "/tmp/mash_features.out"
-  |> generate_mash_feature_file_for_theory thy false
+  "/tmp/mash_accessibility.out"
+  |> generate_mash_accessibility_file_for_theory thy false
 else
   ()
 *}
diff -r f2dd90cc724b -r 288effe53e19 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Tue Jul 10 18:41:34 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -46,8 +46,10 @@
     "\\" ^ stringN_of_int 3 (Char.ord c)
 val escape_meta = String.translate escape_meta_char
 
+val thy_prefix = "y_"
+
 val fact_name_of = escape_meta
-val thy_name_of = escape_meta
+val thy_name_of = prefix thy_prefix o escape_meta
 val const_name_of = prefix const_prefix o escape_meta
 val type_name_of = prefix type_const_prefix o escape_meta
 val class_name_of = prefix class_prefix o escape_meta
@@ -131,7 +133,7 @@
 
 fun parent_thms thy_ths thy =
   Theory.parents_of thy
-  |> map (thy_name_of o Context.theory_name)
+  |> map Context.theory_name
   |> map_filter (AList.lookup (op =) thy_ths)
   |> map List.last
   |> map (fact_name_of o Thm.get_name_hint)
@@ -210,6 +212,7 @@
 (* TODO: Add types, subterms *)
 fun features_of thy (status, th) =
   let val prop = Thm.prop_of th in
+    thy_name_of (thy_name_of_thm th) ::
     interesting_const_names thy prop @
     interesting_type_and_class_names prop
     |> (fn feats =>