src/HOL/Tools/hologic.ML
changeset 34962 807f6ce0273d
parent 33245 65232054ffd0
child 34974 18b41bba42b5
--- a/src/HOL/Tools/hologic.ML	Fri Jan 22 13:39:00 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Fri Jan 22 16:56:51 2010 +0100
@@ -426,7 +426,7 @@
 
 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