changeset 42494 | eef1a23c9077 |
parent 42482 | 42c7ef050bc3 |
child 42496 | 65ec88b369fd |
--- a/src/Pure/Isar/local_defs.ML Wed Apr 27 20:37:56 2011 +0200 +++ b/src/Pure/Isar/local_defs.ML Wed Apr 27 20:58:40 2011 +0200 @@ -92,7 +92,7 @@ let val ((bvars, mxs), specs) = defs |> split_list |>> split_list; val ((bfacts, atts), rhss) = specs |> split_list |>> split_list; - val xs = map Variable.name bvars; + val xs = map Variable.check_name 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;