diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -193,7 +193,7 @@
 text {* definition of a subcontext *}
 
 abbreviation
-  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80)
+  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) where
   "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2"
 
 text {* Now it comes: The Weakening Lemma *}