--- a/src/HOL/Tools/split_rule.ML Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/split_rule.ML Thu Jul 01 16:54:44 2010 +0200
@@ -31,7 +31,7 @@
(*In ap_split S T u, term u expects separate arguments for the factors of S,
with result type T. The call creates a new term expecting one argument
of type S.*)
-fun ap_split (Type (@{type_name "*"}, [T1, T2])) T3 u =
+fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u =
internal_split_const (T1, T2, T3) $
Abs ("v", T1,
ap_split T2 T3