# HG changeset patch
# User berghofe
# Date 1008856749 -3600
# Node ID f2a87c62b4aed1136727b21269b4b2900f390c8e
# Parent  bb2e4689347e8d139660e60896e9437585ddc8e1
cast_ok no longer disabled (thanks to improvement of code generator).

diff -r bb2e4689347e -r f2a87c62b4ae src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 14:58:18 2001 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 14:59:09 2001 +0100
@@ -66,7 +66,6 @@
 
 consts_code
   "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
-  "cast_ok" ("true????")
 
   "wf" ("true?")