# HG changeset patch
# User wenzelm
# Date 1236246843 -3600
# Node ID 18ce07e05a957ddc0b6f1812af4bba9d13c9a59d
# Parent  4f2b6ccce047551bde48f09b7797a69c9cce0cde
Binding.prefix_of;

diff -r 4f2b6ccce047 -r 18ce07e05a95 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Mar 05 10:53:49 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Mar 05 10:54:03 2009 +0100
@@ -188,7 +188,7 @@
     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;