1.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Dec 20 14:59:09 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Dec 20 15:00:02 2001 +0100
     1.3 @@ -87,8 +87,6 @@
     1.4  
     1.5  consts_code
     1.6    "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
     1.7 -  "cast_ok" ("true????")
     1.8 -  "match_exception_entry" ("true????")
     1.9  
    1.10    "wf" ("true?")
    1.11