avoid mixed l/r infixes, which do not work in some versions of SML;
authorwenzelm
Thu, 01 Oct 2009 14:11:28 +0200
changeset 32809 e72347dd3e64
parent 32808 0059238fe4bc
child 32810 f3466a5645fa
child 32820 02f412281b99
avoid mixed l/r infixes, which do not work in some versions of SML;
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*)