1.1 --- a/src/Pure/axclass.ML	Thu Mar 12 12:04:27 2009 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Mar 12 13:18:42 2009 +0100
     1.3 @@ -370,7 +370,7 @@
     1.4      val T' = Type.strip_sorts T;
     1.5    in
     1.6      thy
     1.7 -    |> Sign.sticky_prefix name_inst
     1.8 +    |> Sign.mandatory_path name_inst
     1.9      |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
    1.10      |-> (fn const' as Const (c'', _) =>
    1.11        Thm.add_def false true
    1.12 @@ -480,7 +480,7 @@
    1.13      val class_triv = Thm.class_triv def_thy class;
    1.14      val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
    1.15        def_thy
    1.16 -      |> Sign.sticky_prefix (Binding.name_of bconst)
    1.17 +      |> Sign.mandatory_path (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, [])]),