--- a/src/HOL/MicroJava/J/JBasis.thy Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy Wed Dec 21 12:02:57 2005 +0100
@@ -12,6 +12,7 @@
theory JBasis imports Main begin
lemmas [simp] = Let_def
+declare not_None_eq [iff]
section "unique"