src/HOL/Tools/hologic.ML
changeset 34962 807f6ce0273d
parent 33245 65232054ffd0
child 34974 18b41bba42b5
     1.1 --- a/src/HOL/Tools/hologic.ML	Fri Jan 22 13:39:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/hologic.ML	Fri Jan 22 16:56:51 2010 +0100
     1.3 @@ -426,7 +426,7 @@
     1.4  
     1.5  val strip_psplits =
     1.6    let
     1.7 -    fun strip [] qs Ts t = (t, Ts, qs)
     1.8 +    fun strip [] qs Ts t = (t, rev Ts, qs)
     1.9        | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
    1.10            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
    1.11        | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t