# HG changeset patch
# User blanchet
# Date 1332265365 -3600
# Node ID b86864a2b16e6b916ec4426f5856b89d525c430f
# Parent  7585d0120f1dca8a35dd904f69844eeed6c19e2e
removed obsolete temporary hack

diff -r 7585d0120f1d -r b86864a2b16e src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 20 18:42:45 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 20 18:42:45 2012 +0100
@@ -569,10 +569,8 @@
       filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
     val conjs =
       filt (formula (curry (op =) Conjecture)) |> separate [""] |> flat
-    (* The second layer of ")." is a temporary workaround for a quirk in SPASS's
-       parser. *)
     val settings =
-      (if is_lpo then ["set_flag(Ordering, 1).)."] else []) @
+      (if is_lpo then ["set_flag(Ordering, 1)."] else []) @
       (if gen_prec then
          [ord_info |> map fst |> rev |> commas
                    |> maybe_enclose "set_precedence(" ")."]