--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Feb 11 22:19:58 2010 +0100
@@ -27,14 +27,14 @@
parse_translation {*
let
- fun cart t u = Syntax.const @{type_name cart} $ t $ u
+ fun cart t u = Syntax.const @{type_name cart} $ t $ u; (* FIXME @{type_syntax} *)
fun finite_cart_tr [t, u as Free (x, _)] =
- if Syntax.is_tid x
- then cart t (Syntax.const "_ofsort" $ u $ Syntax.const (hd @{sort finite}))
+ if Syntax.is_tid x then
+ cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const (hd @{sort finite}))
else cart t u
| finite_cart_tr [t, u] = cart t u
in
- [("_finite_cart", finite_cart_tr)]
+ [(@{syntax_const "_finite_cart"}, finite_cart_tr)]
end
*}