src/HOL/Library/LaTeXsugar.thy
changeset 31462 4fcbf17b5a98
parent 30663 0b6aff7451b2
child 35251 e244adbbc28f
--- 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>"