src/HOL/MicroJava/J/JListExample.thy
changeset 18679 cf9f1584431a
parent 17145 e623e57b0f44
child 22921 475ff421a6a3
     1.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Sat Jan 14 17:14:06 2006 +0100
     1.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Sat Jan 14 17:14:11 2006 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4    in nr 0 end;
     1.5  *}
     1.6  
     1.7 -  "arbitrary" ("(raise ERROR)")
     1.8 +  "arbitrary" ("(raise Match)")
     1.9    "arbitrary" :: "val" ("{* Unit *}")
    1.10    "arbitrary" :: "cname" ("\"\"")
    1.11