src/Pure/Isar/class.ML

       val rhs' = Morphism.term phi rhs;
       val same_shape = Term.aconv_untyped (rhs, rhs');
       val is_plain = guess_morphism_identity (b, rhs) Morphism.identity phi;
       val is_canonical = guess_morphism_identity (b, rhs) phi0 phi;
     in
-      not (is_plain orelse is_canonical) ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs')
+      not (is_plain orelse is_canonical) ? Generic_Target.generic_const same_shape prmode ((b', NoSyn), rhs')
     end);
 
 fun dangling_params_for lthy class (type_params, term_params) =
   let
     val class_param_names =