--- a/src/Pure/Isar/local_defs.ML Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML Tue Mar 03 18:32:01 2009 +0100
@@ -90,8 +90,8 @@
let
val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
- val xs = map Binding.base_name bvars;
- val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
+ val xs = map Binding.name_of bvars;
+ val names = map2 (Binding.map_name o Thm.def_name_optional) xs bfacts;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
in