definition in class: provide explicit auxiliary abbreviation carrying potential mixfix syntax in presence of dangling parameters

--- a/src/Pure/Isar/class.ML	Sun Jun 01 08:33:35 2014 +0200
+++ b/src/Pure/Isar/class.ML	Sun Jun 01 14:00:58 2014 +0200
@@ -392,9 +392,10 @@
   in
     lthy
     |> class_const class Syntax.mode_default (b, lhs)
-    |> Local_Theory.raw_theory
-        (canonical_const class phi dangling_params ((Morphism.binding phi b, mx), Morphism.term phi lhs))
-    |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) Syntax.mode_default ((b, NoSyn), lhs)
+    |> Local_Theory.raw_theory (canonical_const class phi dangling_params
+         ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs))
+    |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other)
+         Syntax.mode_default ((b, if null dangling_params then NoSyn else mx), lhs)
     |> synchronize_class_syntax_target class
   end;