src/HOL/MicroJava/J/TypeRel.thy

--- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Aug 28 01:56:40 2003 +0200
@@ -42,7 +42,7 @@
 done
 
 lemma subcls1_def2: 
-"subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
+"subcls1 G = (\<Sigma> C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
   by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
 
 lemma finite_subcls1: "finite (subcls1 G)"