diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Lambda/ListApplication.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -9,7 +9,7 @@
 theory ListApplication imports Lambda begin
 
 abbreviation
-  list_application :: "dB => dB list => dB"    (infixl "\<degree>\<degree>" 150)
+  list_application :: "dB => dB list => dB"  (infixl "\<degree>\<degree>" 150) where
   "t \<degree>\<degree> ts == foldl (op \<degree>) t ts"
 
 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"