src/Pure/Isar/theory_target.ML

     val rhs' = Morphism.term phi rhs;
     val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
     val arg = (b', Term.close_schematic_term rhs');
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
-    val (prefix', _, _) = Binding.dest b';
+    val prefix' = Binding.prefix_of b';
     val class_global = Binding.name_of b = Binding.name_of b'
       andalso not (null prefix')
       andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
   in
     not (is_class andalso (similar_body orelse class_global)) ?