# HG changeset patch
# User kleing
# Date 982838855 -3600
# Node ID 749fd046002f86ac0484e5a8903614185ce871fe
# Parent  dec03152d1636ab12f4db19df7be248a69c9df73
removed unused function

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