# HG changeset patch
# User wenzelm
# Date 1254399088 -7200
# Node ID e72347dd3e647538272028b87deeb65b3618f32a
# Parent  0059238fe4bcfd3f3596406c77c4782450f621f7
avoid mixed l/r infixes, which do not work in some versions of SML;

diff -r 0059238fe4bc -r e72347dd3e64 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Oct 01 12:15:35 2009 +0200
+++ b/src/HOL/Tools/record.ML	Thu Oct 01 14:11:28 2009 +0200
@@ -2121,11 +2121,11 @@
 
     (*cases*)
     val cases_scheme_prop =
-      (All (map dest_Free all_vars_more) (r0 === r_rec0 ==> Trueprop C))
+      (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C))
         ==> Trueprop C;
 
     val cases_prop =
-      (All (map dest_Free all_vars) (r_unit0 === r_rec_unit0 ==> Trueprop C))
+      (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
          ==> Trueprop C;
 
     (*split*)