src/HOL/Tools/refute.ML
changeset 39811 0659e84bdc5f
parent 39809 dac3c3106746
child 40132 7ee65dbffa31
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Oct 01 08:25:23 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Oct 01 10:25:36 2010 +0200
     1.3 @@ -2772,8 +2772,8 @@
     1.4                (* go back up the stack until we find a level where we can go *)
     1.5                (* to the next sibling node                                   *)
     1.6                let
     1.7 -                val offsets' = drop_while
     1.8 -                  (fn off' => off' mod size_elem = size_elem - 1) offsets
     1.9 +                val offsets' = snd (chop_while
    1.10 +                  (fn off' => off' mod size_elem = size_elem - 1) offsets)
    1.11                in
    1.12                  case offsets' of
    1.13                    [] =>