# HG changeset patch
# User kleing
# Date 1008591918 -3600
# Node ID 69971d68fe03c54bebb94a012f6fef0d7a30467f
# Parent  b1ebe0320d796d68d6cb838c3c69f6ad40154c79
fixed JVMListExample

diff -r b1ebe0320d79 -r 69971d68fe03 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Dec 16 00:20:17 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Dec 17 13:25:18 2001 +0100
@@ -83,11 +83,12 @@
   cname ("string")
   vnam ("string")
   mname ("string")
-  loc ("int")
+  loc_ ("int")
 
 consts_code
-  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
+  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
   "cast_ok" ("true????")
+  "match_exception_entry" ("true????")
 
   "wf" ("true?")
 
@@ -104,8 +105,8 @@
   "next_nam" ("\"next\"")
 
 ML {*
-fun new_addr p none hp =
-  let fun nr i = if p (hp i) then (i, none) else nr (i+1);
+fun new_addr p none loc hp =
+  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
   in nr 0 end;
 *}
 
@@ -169,5 +170,4 @@
 ML {* exec (example_prg, the it) *}
 ML {* exec (example_prg, the it) *}
 
-end
-
+end
\ No newline at end of file
diff -r b1ebe0320d79 -r 69971d68fe03 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Sun Dec 16 00:20:17 2001 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Mon Dec 17 13:25:18 2001 +0100
@@ -7,7 +7,7 @@
 use_thy "JTypeSafe";
 use_thy "Example";
 use_thy "JListExample";
-(* use_thy "JVMListExample"; *)
+use_thy "JVMListExample";
 use_thy "BVSpecTypeSafe";
 use_thy "JVM";
 use_thy "LBVSpec";