distinguish updates and queries + cleanups

--- a/src/HOL/TPTP/atp_theory_export.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -37,7 +37,7 @@
 
 fun escape_meta_char c =
   if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
-     c = #")" orelse c = #"?" orelse c = #"," then
+     c = #")" orelse c = #"," then
     String.str c
   else if c = #"'" then
     "~"
@@ -104,14 +104,14 @@
       | do_add_type (TVar (_, S)) = add_classes S
     fun add_type T = type_max_depth >= 0 ? do_add_type T
     fun mk_app s args =
-      if member (op <>) args "?" then s ^ "(" ^ space_implode "," args ^ ")"
+      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
       else s
-    fun patternify ~1 _ = "?"
+    fun patternify ~1 _ = ""
       | patternify depth t =
         case strip_comb t of
           (Const (s, _), args) =>
           mk_app (const_name_of s) (map (patternify (depth - 1)) args)
-        | _ => "?"
+        | _ => ""
     fun add_term_patterns ~1 _ = I
       | add_term_patterns depth t =
         insert (op =) (patternify depth t)
@@ -130,13 +130,8 @@
       end
   in [] |> add_patterns t |> sort string_ord end
 
-val known_tautologies =
-  [@{thm All_def}, @{thm Ex_def}, @{thm Ex1_def}, @{thm Ball_def},
-   @{thm Bex_def}, @{thm If_def}]
-
 fun is_likely_tautology th =
-  (member Thm.eq_thm_prop known_tautologies th orelse
-   th |> prop_of |> interesting_terms_types_and_classes 0 ~1 |> null) andalso
+  null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
   not (Thm.eq_thm_prop (@{thm ext}, th))
 
 fun is_too_meta thy th =
@@ -302,14 +297,14 @@
         val name = Thm.get_name_hint th
         val feats = features_of thy (status, th)
         val deps = dependencies_of all_names th
-        val th = fact_name_of name
-        val s =
-          th ^ ": " ^
-          space_implode " " prevs ^ "; " ^
-          space_implode " " feats ^ "; " ^
-          space_implode " " deps ^ "\n"
-        val _ = File.append path s
-      in [th] end
+        val kind = Thm.legacy_get_kind th
+        val name = fact_name_of name
+        val core =
+          name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats
+        val query = if kind <> "" then "? " ^ core ^ "\n" else ""
+        val update = "! " ^ core ^ "; " ^ space_implode " " deps ^ "\n"
+        val _ = File.append path (query ^ update)
+      in [name] end
     val thy_ths = old_facts |> thms_by_thy
     val parents = parent_thms thy_ths thy
     val _ = fold do_fact new_facts parents