src/HOL/Tools/ATP/atp_proof.ML

   $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
   || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode))
     -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) ""
     >> op ^
 
-val skip_term =
+fun skip_term x =
   let
     fun skip _ accum [] = (accum, [])
       | skip n accum (ss as s :: ss') =
         if (s = "," orelse s = ".") andalso n = 0 then
           (accum, ss)

         else if member (op =) ["(", "["] s then
           skip (n + 1) (s :: accum) ss'
         else
           skip n (s :: accum) ss'
   in
-    skip 0 [] #>> (rev #> implode)
+    (skip 0 [] #>> (rev #> implode)) x
   end
+and skip_terms x = (skip_term ::: Scan.repeat ($$ "," |-- skip_term)) x
 
 datatype source =
   File_Source of string * string option |
   Inference_Source of string * string list |
   Introduced_Source of string

 fun parse_class x = scan_general_id x
 and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x
 
 fun parse_type x =
   (($$ "(" |-- parse_type --| $$ ")"
-    || Scan.this_string tptp_pi_binder |-- $$ "[" |-- skip_term --| $$ "]" --| $$ ":" -- parse_type
+    || Scan.this_string tptp_pi_binder |-- $$ "[" |-- skip_terms --| $$ "]" --| $$ ":" -- parse_type
        >> (fn (_, ty) => ty (* currently ignoring type constructor declarations anyway *))
     || (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") [])
         -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
        >> AType)
    -- Scan.option (($$ tptp_app || $$ tptp_fun_type || $$ tptp_product_type) -- parse_type)