src/Pure/Isar/theory_target.ML
changeset 28941 128459bd72d2
parent 28861 f53abb0733ee
child 28965 1de908189869
--- a/src/Pure/Isar/theory_target.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -201,7 +201,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', _) = Name.dest_binding b';
+    val (prefix', _) = Binding.dest_binding b';
     val class_global = Name.name_of b = Name.name_of b'
       andalso not (null prefix')
       andalso (fst o snd o split_last) prefix' = Class.class_prefix target;