src/HOL/Tools/hologic.ML
changeset 34962 807f6ce0273d
parent 33245 65232054ffd0
child 34974 18b41bba42b5
equal deleted inserted replaced
34947:e1b8f2736404 34962:807f6ce0273d
   424           in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   424           in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   425   in ap [([], T)] end;
   425   in ap [([], T)] end;
   426 
   426 
   427 val strip_psplits =
   427 val strip_psplits =
   428   let
   428   let
   429     fun strip [] qs Ts t = (t, Ts, qs)
   429     fun strip [] qs Ts t = (t, rev Ts, qs)
   430       | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
   430       | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
   431           strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
   431           strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
   432       | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
   432       | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
   433       | strip (p :: ps) qs Ts t = strip ps qs
   433       | strip (p :: ps) qs Ts t = strip ps qs
   434           (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)
   434           (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)