src/Pure/Isar/local_defs.ML

--- a/src/Pure/Isar/local_defs.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -90,7 +90,7 @@
   let
     val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
     val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
-    val xs = map Binding.name_of bvars;
+    val xs = map Name.of_binding bvars;
     val names = map2 Thm.def_binding_optional bvars bfacts;
     val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;