# HG changeset patch
# User ballarin
# Date 1273756182 -7200
# Node ID 9063a5b2b2bbc55aa96a3001a26fd9cff054ede9
# Parent  9eff24f4e5dbf7d9679b90edfa70b254119e8744
Fix syntax; apparently constant apply was introduced in an earlier changeset.

diff -r 9eff24f4e5db -r 9063a5b2b2bb src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Thu May 13 14:47:15 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Thu May 13 15:09:42 2010 +0200
@@ -16,7 +16,7 @@
   below and constants declared in HOL!
 *}
 
-hide_const (open) subset member quotient union inter
+hide_const (open) subset member quotient union inter "apply"
 
 text {*
   Test data for the MESON proof procedure