src/HOL/NanoJava/TypeRel.thy

--- a/src/HOL/NanoJava/TypeRel.thy	Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy	Thu Mar 12 14:58:32 2015 +0100
@@ -108,7 +108,7 @@
 done
 
 --{* Methods of a class, with inheritance and hiding *}
-definition method :: "cname => (mname \<rightharpoonup> methd)" where
+definition "method" :: "cname => (mname \<rightharpoonup> methd)" where
   "method C \<equiv> class_rec C methods"
 
 lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>