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