--- a/src/HOL/MicroJava/J/JListExample.thy Fri Feb 17 11:24:39 2012 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy Fri Feb 17 15:42:26 2012 +0100
@@ -8,7 +8,7 @@
imports Eval
begin
-declare [[syntax_ambiguity = ignore]]
+declare [[syntax_ambiguity_warning = false]]
consts
list_nam :: cnam