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