--- 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(" ")."]