# 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*)