# HG changeset patch
# User haftmann
# Date 1226649011 -3600
# Node ID bb7a102e2f5db1b914227c1ecc7f8da4cd160520
# Parent  1d80cee865defca0be190052cbaea083b7d4b7b1
re-educated guess

diff -r 1d80cee865de -r bb7a102e2f5d src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Nov 14 08:50:10 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Nov 14 08:50:11 2008 +0100
@@ -186,14 +186,14 @@
   let
     val c' = Morphism.name phi c;
     val rhs' = Morphism.term phi rhs;
-    val name = Name.name_of c;
     val name' = Name.name_of c';
     val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
     val arg = (name', Term.close_schematic_term rhs');
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
-    val class_global = name = NameSpace.base name'
-      andalso Class.class_prefix target = hd (NameSpace.explode name');
+    val class_global = Name.name_of c = Name.name_of c'
+      andalso not (null (Name.prefix_of c'))
+      andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target;
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result