src/HOL/Tools/record.ML
changeset 32809 e72347dd3e64
parent 32808 0059238fe4bc
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Tools/record.ML	Thu Oct 01 12:15:35 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Thu Oct 01 14:11:28 2009 +0200
     1.3 @@ -2121,11 +2121,11 @@
     1.4  
     1.5      (*cases*)
     1.6      val cases_scheme_prop =
     1.7 -      (All (map dest_Free all_vars_more) (r0 === r_rec0 ==> Trueprop C))
     1.8 +      (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C))
     1.9          ==> Trueprop C;
    1.10  
    1.11      val cases_prop =
    1.12 -      (All (map dest_Free all_vars) (r_unit0 === r_rec_unit0 ==> Trueprop C))
    1.13 +      (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
    1.14           ==> Trueprop C;
    1.15  
    1.16      (*split*)