diff -r 26d349416c4f -r a718f1ccaf1a src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Nov 10 14:31:21 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sat Nov 10 14:31:22 2007 +0100
@@ -177,15 +177,16 @@
     val rhs' = Morphism.term phi rhs;
     val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
     val arg = (c', Term.close_schematic_term rhs');
+    val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
-    val class_global = is_class andalso c' = NameSpace.qualified (Class.class_prefix target) c;
+    val class_global = c' = NameSpace.qualified (Class.class_prefix target) c;
   in
-    not class_global ?
+    not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
         (Sign.add_abbrev PrintMode.internal pos legacy_arg)
         (ProofContext.add_abbrev PrintMode.internal pos arg)
       #-> (fn (lhs' as Const (d, _), _) =>
-          Type.similar_types (rhs, rhs') ?
+          similar_body ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   end;