src/Pure/axclass.ML
changeset 30468 0cf8f536ef98
parent 30364 577edc39b501
child 30469 de9e8f1d927c
     1.1 --- a/src/Pure/axclass.ML	Thu Mar 12 11:17:34 2009 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Mar 12 12:04:27 2009 +0100
     1.3 @@ -371,7 +371,6 @@
     1.4    in
     1.5      thy
     1.6      |> Sign.sticky_prefix name_inst
     1.7 -    |> Sign.no_base_names
     1.8      |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
     1.9      |-> (fn const' as Const (c'', _) =>
    1.10        Thm.add_def false true
    1.11 @@ -481,8 +480,7 @@
    1.12      val class_triv = Thm.class_triv def_thy class;
    1.13      val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
    1.14        def_thy
    1.15 -      |> Sign.add_path (Binding.name_of bconst)
    1.16 -      |> Sign.no_base_names
    1.17 +      |> Sign.sticky_prefix (Binding.name_of bconst)
    1.18        |> PureThy.note_thmss ""
    1.19          [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
    1.20           ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),