--- a/src/Pure/axclass.ML Thu Mar 12 12:04:27 2009 +0100
+++ b/src/Pure/axclass.ML Thu Mar 12 13:18:42 2009 +0100
@@ -370,7 +370,7 @@
val T' = Type.strip_sorts T;
in
thy
- |> Sign.sticky_prefix name_inst
+ |> Sign.mandatory_path name_inst
|> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
|-> (fn const' as Const (c'', _) =>
Thm.add_def false true
@@ -480,7 +480,7 @@
val class_triv = Thm.class_triv def_thy class;
val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
def_thy
- |> Sign.sticky_prefix (Binding.name_of bconst)
+ |> Sign.mandatory_path (Binding.name_of bconst)
|> PureThy.note_thmss ""
[((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),