--- a/src/HOL/MicroJava/BV/Effect.thy Wed Dec 02 12:04:07 2009 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Tue Nov 24 14:37:23 2009 +0100
@@ -9,7 +9,6 @@
imports JVMType "../JVM/JVMExceptions"
begin
-
types
succ_type = "(p_count \<times> state_type option) list"