# HG changeset patch
# User paulson
# Date 1113056831 -7200
# Node ID adf0ba6353f3138a225370b11576c11f9fd88ee8
# Parent  8fa8872cdc49e8d710fe8ff654fb9a2da152df01
fixed the syntax of infix declarations

diff -r 8fa8872cdc49 -r adf0ba6353f3 src/HOL/Tools/ATP/recon_parse.ML
--- a/src/HOL/Tools/ATP/recon_parse.ML	Sat Apr 09 15:36:02 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML	Sat Apr 09 16:27:11 2005 +0200
@@ -26,7 +26,7 @@
 exception Noparse;
 exception SPASSError of string;
 
-fun ++ (parser1, parser2) input =
+fun (parser1 ++ parser2) input =
       let
         val (result1, rest1) = parser1 input
         val (result2, rest2) = parser2 rest1
@@ -47,14 +47,14 @@
 
 
 
-fun >> (parser, treatment) input =
+fun (parser >> treatment) input =
       let
         val (result, rest) = parser input
       in
         (treatment result, rest)
       end;
 
-fun || (parser1, parser2) input = parser1 input
+fun (parser1 || parser2) input = parser1 input
 handle Noparse => parser2 input;
 
 infixr 8 ++; infixr 7 >>; infixr 6 ||;