
diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Mon Jan 03 14:07:08 2000 +0100
@@ -26,7 +26,7 @@
   hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
  "G\\<turnstile>h h\\<surd>    \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
 
-  conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
+  conforms :: "state \\<Rightarrow> java_mb env \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
  "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
 
 end




