# HG changeset patch
# User kleing
# Date 1008458324 -3600
# Node ID 521f2da133bedb938f307d7897ecf3df60f1dfcc
# Parent  360e3215f029365b795c9c6788abaa00e55d1a18
exception merge, doesn't work yet

diff -r 360e3215f029 -r 521f2da133be src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Dec 16 00:18:17 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Dec 16 00:18:44 2001 +0100
@@ -22,7 +22,7 @@
   next_name :: vname
   "next_name == VName next_nam"
 
-  list_class :: "(nat * nat * bytecode) class"
+  list_class :: "jvm_method class"
   "list_class ==
     (Object,
      [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
@@ -41,9 +41,9 @@
         Load 1,
         Putfield next_name list_name,
         LitPush Unit,
-        Return]))])"
+        Return],[]))])"
 
-  test_class :: "(nat * nat * bytecode) class"
+  test_class :: "jvm_method class"
   "test_class ==
     (Object, [],
      [((makelist_name, []), PrimT Integer,
@@ -70,7 +70,7 @@
         Load 2,
         Invoke list_name append_name [RefT (ClassT list_name)],
         LitPush Unit,
-        Return]))])"
+        Return],[]))])"
 
   example_prg :: jvm_prog
   "example_prg == [ObjectC, (list_name, list_class), (test_name, test_class)]"