--- a/src/HOL/Tools/ATP/atp_proof.ML Mon May 02 15:01:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon May 02 15:13:10 2011 +0200
@@ -352,8 +352,8 @@
val parse_vampire_braced_stuff =
$$ "{" -- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) -- $$ "}"
-val parse_vampire_parenthesized_detritus =
- $$ "(" |-- parse_vampire_detritus --| $$ ")"
+fun parse_vampire_parenthesized_detritus x =
+ ($$ "(" |-- parse_vampire_detritus --| $$ ")") x
(* Syntax: <num>. <formula> <annotation> *)
fun parse_vampire_line x =