src/HOL/Tools/record.ML
changeset 32809 e72347dd3e64
parent 32808 0059238fe4bc
child 32952 aeb1e44fbc19
--- 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*)