--- a/src/HOL/MicroJava/J/JListExample.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Tue Oct 07 16:07:50 2008 +0200
@@ -5,7 +5,9 @@
header {* \isaheader{Example for generating executable code from Java semantics} *}
-theory JListExample imports Eval SystemClasses begin
+theory JListExample
+imports Eval SystemClasses
+begin
ML {* Syntax.ambiguity_level := 100000 *}
@@ -72,9 +74,9 @@
in nr 0 end;
*}
- "arbitrary" ("(raise Match)")
- "arbitrary :: val" ("{* Unit *}")
- "arbitrary :: cname" ("\"\"")
+ "undefined" ("(raise Match)")
+ "undefined :: val" ("{* Unit *}")
+ "undefined :: cname" ("\"\"")
"Object" ("\"Object\"")
"list_name" ("\"list\"")