diff -r 0aaeea9255f3 -r 6267ad688ea8 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Tue Jan 26 14:08:47 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Jan 26 14:48:25 2010 +0100
@@ -511,6 +511,14 @@
            end
        end 
 
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, Abs(v1', ty', s1))),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , Abs(v2', _  , s2)))) =>
+       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, Abs(v1', ty', regularize_trm ctxt (s1, s2)))
+
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, s1)),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , s2))) =>
+       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, regularize_trm ctxt (s1, s2))
+
   | (t1 $ t2, t1' $ t2') =>
        (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2'))