--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Apr 08 16:34:14 2011 +0200
@@ -32,7 +32,7 @@
let
fun cart t u = Syntax.const @{type_syntax cart} $ t $ u;
fun finite_cart_tr [t, u as Free (x, _)] =
- if Syntax.is_tid x then
+ if Lexicon.is_tid x then
cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite})
else cart t u
| finite_cart_tr [t, u] = cart t u