src/HOL/Tools/refute.ML
changeset 48902 44a6967240b7
parent 46961 5c6955f487e5
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Aug 23 12:55:23 2012 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Aug 23 13:03:29 2012 +0200
     1.3 @@ -2772,7 +2772,7 @@
     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' = snd (chop_while
     1.8 +                val offsets' = snd (take_prefix
     1.9                    (fn off' => off' mod size_elem = size_elem - 1) offsets)
    1.10                in
    1.11                  case offsets' of