# HG changeset patch
# User berghofe
# Date 1120219866 -7200
# Node ID 701218c1301cc9156d7a4c851e5eec53baf7199b
# Parent  39cb9fe20fe373eed33ecde4b7b8c3f73c6c289c
Corrected implementation of arbitrary on cname.

diff -r 39cb9fe20fe3 -r 701218c1301c src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Jul 01 14:10:02 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Jul 01 14:11:06 2005 +0200
@@ -98,7 +98,7 @@
 
   "arbitrary" ("(raise ERROR)")
   "arbitrary" :: "val" ("{* Unit *}")
-  "arbitrary" :: "cname" ("Object")
+  "arbitrary" :: "cname" ("{* Object *}")
 
   "list_nam" ("\"list\"")
   "test_nam" ("\"test\"")
@@ -115,7 +115,7 @@
 
 subsection {* Single step execution *}
 
-generate_code 
+generate_code
   test = "exec (E, start_state E test_name makelist_name)"
 
 ML {* test *}