--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 22:09:50 2010 +0100
@@ -19,9 +19,8 @@
comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a"
"comb_nil a == ([], a)"
-syntax (xsymbols)
- "comb" :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"
- (infixr "\<box>" 55)
+notation (xsymbols)
+ comb (infixr "\<box>" 55)
lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
by (simp add: comb_def comb_nil_def split_beta)