# HG changeset patch
# User haftmann
# Date 1401624058 -7200
# Node ID 4069c9b3803a3c7538861ec9da04edbe37cb4ca2
# Parent  9d6f733ef45647353c9a0221b2738f653a97944f
definition in class: provide explicit auxiliary abbreviation carrying potential mixfix syntax in presence of dangling parameters

diff -r 9d6f733ef456 -r 4069c9b3803a src/Pure/Isar/class.ML
--- 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;