src/Pure/Isar/class.ML

 local
 
 fun guess_morphism_identity (b, rhs) phi1 phi2 =
   let
     (*FIXME proper concept to identify morphism instead of educated guess*)
-    val name_of_binding = Name_Space.full_name Name_Space.default_naming;
+    val name_of_binding = Name_Space.full_name Name_Space.global_naming;
     val n1 = (name_of_binding o Morphism.binding phi1) b;
     val n2 = (name_of_binding o Morphism.binding phi2) b;
     val rhs1 = Morphism.term phi1 rhs;
     val rhs2 = Morphism.term phi2 rhs;
   in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end;