--- a/src/HOL/Tools/TFL/usyntax.ML Wed Jul 29 16:43:02 2009 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Wed Jul 29 16:48:34 2009 +0200
@@ -118,7 +118,7 @@
val alpha = mk_vartype "'a"
val beta = mk_vartype "'b"
-val strip_prod_type = HOLogic.prodT_factors;
+val strip_prod_type = HOLogic.flatten_tupleT;