diff -r dec03152d163 -r 749fd046002f src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Thu Feb 22 11:31:31 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Thu Feb 22 11:47:35 2001 +0100
@@ -40,10 +40,4 @@
 types
   jvm_state = "xcpt option \<times> aheap \<times> frame list"	
 
-
-text {* dynamic method lookup: *}
-constdefs
-  dyn_class	:: "'code prog \<times> sig \<times> cname => cname"
-  "dyn_class == \<lambda>(G,sig,C). fst(the(method(G,C) sig))"
-
 end