# HG changeset patch
# User haftmann
# Date 1281355643 -7200
# Node ID 7b6ecb6070dc450c51ef257bad7623b15ed85aa8
# Parent  62abd53f37fa11dc592e815c9c61aaa179fcfd56
sharpened and tuned educated guess for canonical class morphism

diff -r 62abd53f37fa -r 7b6ecb6070dc src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Aug 09 13:43:01 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Aug 09 14:07:23 2010 +0200
@@ -217,12 +217,13 @@
     val same_shape = Term.aconv_untyped (rhs, rhs');
     (* FIXME workaround based on educated guess *)
     val prefix' = Binding.prefix_of b';
-    val class_global =
-      Binding.eq_name (b, b') andalso
-      not (null prefix') andalso
-      fst (snd (split_last prefix')) = Class_Target.class_prefix target;
+    val is_canonical_class = is_class andalso
+      (Binding.eq_name (b, b')
+        andalso not (null prefix')
+        andalso List.last prefix' = (Class_Target.class_prefix target, false) (*guesses class constants*)
+      orelse same_shape (*guesses class abbrevs*));
   in
-    not (is_class andalso (same_shape orelse class_global)) ?
+    not is_canonical_class ?
       (Context.mapping_result
         (Sign.add_abbrev Print_Mode.internal arg)
         (ProofContext.add_abbrev Print_Mode.internal arg)