# HG changeset patch
# User wenzelm
# Date 1266782657 -3600
# Node ID 0f17eda72e602059495703c3c6b02574fed05153
# Parent  68dd8b51c6b81c271593e3670b5f679cbc147be1
binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;

diff -r 68dd8b51c6b8 -r 0f17eda72e60 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Feb 21 20:55:12 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Feb 21 21:04:17 2010 +0100
@@ -14,9 +14,9 @@
   ('a, 'b) cart = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
   morphisms Cart_nth Cart_lambda ..
 
-notation Cart_nth (infixl "$" 90)
-
-notation (xsymbols) Cart_lambda (binder "\<chi>" 10)
+notation
+  Cart_nth (infixl "$" 90) and
+  Cart_lambda (binder "\<chi>" 10)
 
 (*
   Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than