# HG changeset patch
# User huffman
# Date 1235777876 28800
# Node ID f65dc19cd5f050c22cc5ffcba351991359206411
# Parent  98a986b02022f92d5e6cebab5d31a0976723f73b
make list-style polynomial syntax work when show_sorts is on

diff -r 98a986b02022 -r f65dc19cd5f0 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Feb 27 16:05:40 2009 +0100
+++ b/src/HOL/Library/Polynomial.thy	Fri Feb 27 15:37:56 2009 -0800
@@ -106,6 +106,7 @@
 translations
   "[:x, xs:]" == "CONST pCons x [:xs:]"
   "[:x:]" == "CONST pCons x 0"
+  "[:x:]" <= "CONST pCons x (_constrain 0 t)"
 
 lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"
   unfolding Poly_def by (auto split: nat.split)