--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Thu Aug 25 16:10:16 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Thu Aug 25 16:13:09 2005 +0200
@@ -114,62 +114,63 @@
subsection {* Single step execution *}
-generate_code
+code_module JVM
+contains
test = "exec (E, start_state E test_name makelist_name)"
-ML {* test *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
+ML {* JVM.test *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
end