# HG changeset patch
# User haftmann
# Date 1244183304 -7200
# Node ID 4fcbf17b5a98cd529843abbf0d86211c4b6fec4e
# Parent  d54b743b52a308e534c36313167ac5c7ba0743f0
Set.insert with authentic syntax

diff -r d54b743b52a3 -r 4fcbf17b5a98 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Fri Jun 05 08:06:03 2009 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jun 05 08:28:24 2009 +0200
@@ -34,7 +34,7 @@
 
 (* insert *)
 translations 
-  "{x} \<union> A" <= "insert x A"
+  "{x} \<union> A" <= "CONST insert x A"
   "{x,y}" <= "{x} \<union> {y}"
   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
   "{x}" <= "{x} \<union> \<emptyset>"