1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 20 17:20:33 2012 +0000
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 20 18:42:45 2012 +0100
     1.3 @@ -578,20 +578,20 @@
     1.4                     |> maybe_enclose "set_precedence(" ")."]
     1.5         else
     1.6           [])
     1.7 -    fun list_of _ _ _ [] = []
     1.8 -      | list_of heading bef aft ss =
     1.9 -        "list_of_" ^ heading ^ ".\n" :: bef :: map (suffix "\n") ss @
    1.10 -        [aft, "end_of_list.\n\n"]
    1.11 +    fun list_of _ [] = []
    1.12 +      | list_of heading ss =
    1.13 +        "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @
    1.14 +        ["end_of_list.\n\n"]
    1.15    in
    1.16      "\nbegin_problem(isabelle).\n\n" ::
    1.17 -    list_of "descriptions" "" ""
    1.18 +    list_of "descriptions"
    1.19              ["name({**}).", "author({**}).", "status(unknown).",
    1.20               "description({**})."] @
    1.21 -    list_of "symbols" "" "" syms @
    1.22 -    list_of "declarations" "" "" decls @
    1.23 -    list_of "formulae(axioms)" "" "" axioms @
    1.24 -    list_of "formulae(conjectures)" "" "" conjs @
    1.25 -    list_of "settings(SPASS)" "{*\n" "*}\n" settings @
    1.26 +    list_of "symbols" syms @
    1.27 +    list_of "declarations" decls @
    1.28 +    list_of "formulae(axioms)" axioms @
    1.29 +    list_of "formulae(conjectures)" conjs @
    1.30 +    list_of "settings(SPASS)" settings @
    1.31      ["end_problem.\n"]
    1.32    end
    1.33