src/Pure/proofterm.ML

       | shrink' ls lev ts prfs prf =
           let
             val prop = (case prf of PThm (_, _, prop, _) => prop | PAxm (_, prop, _) => prop
               | Oracle (_, prop, _) => prop | _ => error "shrink: proof not in normal form");
             val vs = vars_of prop;
-            val (ts', ts'') = splitAt (length vs, ts)
+            val (ts', ts'') = chop (length vs) ts;
             val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
             val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
               insert (op =) ixn (case AList.lookup (op =) insts ixn of
                   SOME (SOME t) => if is_proj t then ixns union ixns' else ixns'
                 | _ => ixns union ixns'))