diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/MicroJava/Comp/Index.thy
--- a/src/HOL/MicroJava/Comp/Index.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -98,7 +98,7 @@
 
 
 
-(* The following def should replace the conditions in WellType.thy / wf_java_mdecl
+(* The following definition should replace the conditions in WellType.thy / wf_java_mdecl
 *)
 definition disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" where
   "disjoint_varnames pns lvars \<equiv>