# HG changeset patch
# User berghofe
# Date 1008856802 -3600
# Node ID 7fb12775ce98d2c8a7ffbe57da20b4e6a98ebfb6
# Parent  f2a87c62b4aed1136727b21269b4b2900f390c8e
cast_ok and match_exception_entry no longer disabled (thanks to
improvement of code generator).

diff -r f2a87c62b4ae -r 7fb12775ce98 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Dec 20 14:59:09 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Dec 20 15:00:02 2001 +0100
@@ -87,8 +87,6 @@
 
 consts_code
   "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
-  "cast_ok" ("true????")
-  "match_exception_entry" ("true????")
 
   "wf" ("true?")