diff -r fd28b7399f2b -r 06c87d2c5b5a src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Nov 09 19:42:33 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Nov 09 20:47:39 2009 +0100
@@ -190,9 +190,7 @@
     val b' = Morphism.binding phi b;
     val rhs' = Morphism.term phi rhs;
     val arg = (b', Term.close_schematic_term rhs');
-(*    val similar_body = Type.similar_types (rhs, rhs'); *)
-    val same_shape = op aconv o pairself (Term.map_types (fn _ => Term.dummyT));
-    val similar_body = same_shape (rhs, rhs');
+    val same_shape = Term.aconv_untyped (rhs, rhs');
     (* FIXME workaround based on educated guess *)
     val prefix' = Binding.prefix_of b';
     val class_global =
@@ -200,12 +198,12 @@
       not (null prefix') andalso
       fst (snd (split_last prefix')) = Class_Target.class_prefix target;
   in
-    not (is_class andalso (similar_body orelse class_global)) ?
+    not (is_class andalso (same_shape orelse class_global)) ?
       (Context.mapping_result
         (Sign.add_abbrev PrintMode.internal arg)
         (ProofContext.add_abbrev PrintMode.internal arg)
       #-> (fn (lhs' as Const (d, _), _) =>
-          similar_body ?
+          same_shape ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   end;