# HG changeset patch
# User haftmann
# Date 1402263048 -7200
# Node ID 329f7f76f0a416a688205023b7cceeab414e10b6
# Parent  de00494fa8b30e84d038ce7d0359c9ee5f846ea1
revert effect of 63c7b29d29ac -- existing pervasive interpretation of class order for dvd etc. is too obstrusive at the moment

diff -r de00494fa8b3 -r 329f7f76f0a4 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Jun 08 23:30:47 2014 +0200
+++ b/src/Pure/Isar/class.ML	Sun Jun 08 23:30:48 2014 +0200
@@ -342,7 +342,7 @@
       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) =