1.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 14:58:18 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 14:59:09 2001 +0100
     1.3 @@ -66,7 +66,6 @@
     1.4  
     1.5  consts_code
     1.6    "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
     1.7 -  "cast_ok" ("true????")
     1.8  
     1.9    "wf" ("true?")
    1.10