diff -r 62854cac5410 -r 4575c87dd25b src/HOL/Induct/Comb.thy
--- a/src/HOL/Induct/Comb.thy	Fri Apr 22 17:32:03 2005 +0200
+++ b/src/HOL/Induct/Comb.thy	Fri Apr 22 17:32:29 2005 +0200
@@ -39,6 +39,9 @@
   "x -1-> y" == "(x,y) \<in> contract"
   "x ---> y" == "(x,y) \<in> contract^*"
 
+syntax (xsymbols)
+  "op ##" :: "[comb,comb] => comb"  (infixl "\<bullet>" 90)
+
 inductive contract
   intros
     K:     "K##x##y -1-> x"