src/HOL/MicroJava/J/JListExample.thy
changeset 46512 4f9f61f9b535
parent 46506 c7faa011bfa7
child 51272 9c8d63b4b6be
     1.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Fri Feb 17 11:24:39 2012 +0100
     1.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Fri Feb 17 15:42:26 2012 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Eval
     1.5  begin
     1.6  
     1.7 -declare [[syntax_ambiguity = ignore]]
     1.8 +declare [[syntax_ambiguity_warning = false]]
     1.9  
    1.10  consts
    1.11    list_nam :: cnam