src/Pure/Isar/theory_target.ML
changeset 28941 128459bd72d2
parent 28861 f53abb0733ee
child 28965 1de908189869
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Dec 01 16:02:57 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Dec 01 19:41:16 2008 +0100
     1.3 @@ -201,7 +201,7 @@
     1.4      val arg = (b', Term.close_schematic_term rhs');
     1.5      val similar_body = Type.similar_types (rhs, rhs');
     1.6      (* FIXME workaround based on educated guess *)
     1.7 -    val (prefix', _) = Name.dest_binding b';
     1.8 +    val (prefix', _) = Binding.dest_binding b';
     1.9      val class_global = Name.name_of b = Name.name_of b'
    1.10        andalso not (null prefix')
    1.11        andalso (fst o snd o split_last) prefix' = Class.class_prefix target;