# HG changeset patch
# User blanchet
# Date 1304341990 -7200
# Node ID 8d7039b6ad7ab5f541f89eaaf7952f25a9bdd890
# Parent  81953e554197d80ca191fa923248cda66d33e644
make SML/NJ happier

diff -r 81953e554197 -r 8d7039b6ad7a src/HOL/Tools/ATP/atp_proof.ML
--- 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 =