src/Pure/axclass.ML
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);