src/HOL/Tools/record.ML
changeset 33063 4d462963a7db
parent 33055 5a733f325939
child 33095 bbd52d2f8696
     1.1 --- a/src/HOL/Tools/record.ML	Thu Oct 22 10:52:07 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Thu Oct 22 13:48:06 2009 +0200
     1.3 @@ -1894,8 +1894,8 @@
     1.4              more;
     1.5        in
     1.6          if more = HOLogic.unit
     1.7 -        then build (map recT (0 upto parent_len))
     1.8 -        else build (map rec_schemeT (0 upto parent_len))
     1.9 +        then build (map_range recT (parent_len + 1))
    1.10 +        else build (map_range rec_schemeT (parent_len + 1))
    1.11        end;
    1.12  
    1.13      val r_rec0 = mk_rec all_vars_more 0;