src/HOL/MicroJava/J/WellForm.thy

--- a/src/HOL/MicroJava/J/WellForm.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -25,7 +25,7 @@
 \end{itemize}
 \end{description}
 *}
-types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
+type_synonym 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
 
 definition wf_syscls :: "'c prog => bool" where
 "wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"