src/HOL/Tools/hologic.ML

           in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   in ap [([], T)] end;
 
 val strip_psplits =
   let
-    fun strip [] qs Ts t = (t, Ts, qs)
+    fun strip [] qs Ts t = (t, rev Ts, qs)
       | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
           strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
       | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
       | strip (p :: ps) qs Ts t = strip ps qs
           (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)