src/HOL/Tools/refute.ML
changeset 39811 0659e84bdc5f
parent 39809 dac3c3106746
child 40132 7ee65dbffa31
equal deleted inserted replaced
39810:5c9fe600525e 39811:0659e84bdc5f
  2770               (assoc, (offsets, off + 1))
  2770               (assoc, (offsets, off + 1))
  2771             else
  2771             else
  2772               (* go back up the stack until we find a level where we can go *)
  2772               (* go back up the stack until we find a level where we can go *)
  2773               (* to the next sibling node                                   *)
  2773               (* to the next sibling node                                   *)
  2774               let
  2774               let
  2775                 val offsets' = drop_while
  2775                 val offsets' = snd (chop_while
  2776                   (fn off' => off' mod size_elem = size_elem - 1) offsets
  2776                   (fn off' => off' mod size_elem = size_elem - 1) offsets)
  2777               in
  2777               in
  2778                 case offsets' of
  2778                 case offsets' of
  2779                   [] =>
  2779                   [] =>
  2780                     (* we're at the last node in the tree; the next value *)
  2780                     (* we're at the last node in the tree; the next value *)
  2781                     (* won't be used anyway                               *)
  2781                     (* won't be used anyway                               *)