src/Pure/Isar/local_defs.ML
changeset 30223 24d975352879
parent 30211 556d1810cdad
child 30242 aea5d7fa7ef5
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Mar 03 18:31:59 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Mar 03 18:32:01 2009 +0100
     1.3 @@ -90,8 +90,8 @@
     1.4    let
     1.5      val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
     1.6      val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
     1.7 -    val xs = map Binding.base_name bvars;
     1.8 -    val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
     1.9 +    val xs = map Binding.name_of bvars;
    1.10 +    val names = map2 (Binding.map_name o Thm.def_name_optional) xs bfacts;
    1.11      val eqs = mk_def ctxt (xs ~~ rhss);
    1.12      val lhss = map (fst o Logic.dest_equals) eqs;
    1.13    in