# HG changeset patch
# User blanchet
# Date 1306068664 -7200
# Node ID ad34216cff2fab66361480e831c1ffa9843eea0b
# Parent  47f366f1fe32649d93262a9dc4c48ce9eb0728ea
removed SNARK hack now that SNARK is fixed

diff -r 47f366f1fe32 -r ad34216cff2f src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 22 14:51:04 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 22 14:51:04 2011 +0200
@@ -31,6 +31,10 @@
   val tptp_tff_bool_type : string
   val tptp_tff_individual_type : string
   val is_atp_variable : string -> bool
+  val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
+  val mk_aconn :
+    connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
+    -> ('a, 'b, 'c) formula
   val timestamp : unit -> string
   val hashw : word * word -> word
   val hashw_string : string * word -> word
@@ -74,6 +78,10 @@
 
 fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
 
+fun mk_anot (AConn (ANot, [phi])) = phi
+  | mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
 
 (* This hash function is recommended in Compilers: Principles, Techniques, and
@@ -172,7 +180,7 @@
   | open_non_conjecture_line line = line
 
 fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) =
-    Formula (ident, Hypothesis, AConn (ANot, [phi]), source, info)
+    Formula (ident, Hypothesis, mk_anot phi, source, info)
   | negate_conjecture_line line = line
 
 val filter_cnf_ueq_problem =
@@ -218,10 +226,6 @@
   else
     s |> no_qualifiers
       |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
-         (* SNARK 20080805r024 doesn't like sort (type) names that end with
-            digits. We make an effort to avoid this here. *)
-      |> (fn s => if Char.isDigit (String.sub (s, size s - 1)) then s ^ "_"
-                  else s)
       |> (fn s =>
              if size s > max_readable_name_size then
                String.substring (s, 0, max_readable_name_size div 2 - 4) ^
@@ -243,10 +247,8 @@
         val nice_prefix = readable_name full_name desired_name
         fun add j =
           let
-            (* The trailing "_" is for SNARK 20080805r024 (see comment
-               above). *)
             val nice_name =
-              nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j ^ "_")
+              nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j)
           in
             case Symtab.lookup (snd the_pool) nice_name of
               SOME full_name' =>