src/Pure/Isar/local_defs.ML
changeset 30585 6b2ba4666336
parent 30473 e0b66c11e7e4
child 30763 6976521b4263
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Mar 19 13:26:19 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Mar 19 13:28:55 2009 +0100
     1.3 @@ -90,7 +90,7 @@
     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.name_of bvars;
     1.8 +    val xs = map Name.of_binding bvars;
     1.9      val names = map2 Thm.def_binding_optional bvars bfacts;
    1.10      val eqs = mk_def ctxt (xs ~~ rhss);
    1.11      val lhss = map (fst o Logic.dest_equals) eqs;