diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Fri Jul 14 16:32:51 2000 +0200
@@ -6,7 +6,9 @@
 Conformity relations for type safety of Java
 *)
 
-Conform = State +
+Conform = State + WellType +
+
+types	'c env_ = "'c prog \\<times> (vname \\<leadsto> ty)" (* same as env of WellType.thy *)
 
 constdefs
 
@@ -26,7 +28,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> java_mb 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