revert effect of 63c7b29d29ac -- existing pervasive interpretation of class order for dvd etc. is too obstrusive at the moment
--- 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) =