--- a/src/HOL/Bali/WellForm.thy Sat Jan 14 16:12:09 2012 +0100
+++ b/src/HOL/Bali/WellForm.thy Sat Jan 14 16:14:22 2012 +0100
@@ -58,9 +58,9 @@
definition
wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
"wf_mhead G P = (\<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
- \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and>
+ ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and>
is_acc_type G P (resTy mh) \<and>
- \<spacespace> distinct (pars mh))"
+ distinct (pars mh))"
text {*