# HG changeset patch
# User wenzelm
# Date 1267273975 -3600
# Node ID 69e2c0839091898c47e6eab1c2aa03d3dff59423
# Parent  041bb8d18916ea1ca11a641eac0d83f383cc6966
more precise syntax antiquotations;

diff -r 041bb8d18916 -r 69e2c0839091 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat Feb 27 13:32:38 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat Feb 27 13:32:55 2010 +0100
@@ -27,10 +27,10 @@
 
 parse_translation {*
 let
-  fun cart t u = Syntax.const @{type_name cart} $ t $ u;   (* FIXME @{type_syntax} *)
+  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
-          cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const (hd @{sort finite}))
+          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
 in