changeset 35238 | 18ae6ef02fe0 |
parent 35201 | c2ddb9395436 |
child 35669 | a91c7ed801b8 |
--- a/src/Pure/axclass.ML Fri Feb 19 20:39:48 2010 +0100 +++ b/src/Pure/axclass.ML Fri Feb 19 20:41:34 2010 +0100 @@ -474,7 +474,7 @@ val ([def], def_thy) = thy |> Sign.primitive_class (bclass, super) - |> PureThy.add_defs false [((Binding.map_name Thm.def_name bconst, class_eq), [])]; + |> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])]; val (raw_intro, (raw_classrel, raw_axioms)) = split_defined (length conjs) def ||> chop (length super);