replaced old-style add_path/no_base_names by sticky_prefix;
authorwenzelm
Thu Mar 12 12:04:27 2009 +0100 (2009-03-12 ago)
changeset 304680cf8f536ef98
parent 30467 afd0e5095c6b
child 30469 de9e8f1d927c
replaced old-style add_path/no_base_names by sticky_prefix;
src/Pure/Isar/expression.ML
src/Pure/axclass.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Mar 12 11:17:34 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Mar 12 12:04:27 2009 +0100
     1.3 @@ -674,8 +674,7 @@
     1.4              |> def_pred aname parms defs' exts exts';
     1.5            val (_, thy'') =
     1.6              thy'
     1.7 -            |> Sign.add_path (Binding.name_of aname)
     1.8 -            |> Sign.no_base_names
     1.9 +            |> Sign.sticky_prefix (Binding.name_of aname)
    1.10              |> PureThy.note_thmss Thm.internalK
    1.11                [((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])]
    1.12              ||> Sign.restore_naming thy';
    1.13 @@ -689,8 +688,7 @@
    1.14              |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
    1.15            val (_, thy'''') =
    1.16              thy'''
    1.17 -            |> Sign.add_path (Binding.name_of pname)
    1.18 -            |> Sign.no_base_names
    1.19 +            |> Sign.sticky_prefix (Binding.name_of pname)
    1.20              |> PureThy.note_thmss Thm.internalK
    1.21                   [((Binding.name introN, []), [([intro], [Locale.intro_attrib])]),
    1.22                    ((Binding.name axiomsN, []),
     2.1 --- a/src/Pure/axclass.ML	Thu Mar 12 11:17:34 2009 +0100
     2.2 +++ b/src/Pure/axclass.ML	Thu Mar 12 12:04:27 2009 +0100
     2.3 @@ -371,7 +371,6 @@
     2.4    in
     2.5      thy
     2.6      |> Sign.sticky_prefix name_inst
     2.7 -    |> Sign.no_base_names
     2.8      |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
     2.9      |-> (fn const' as Const (c'', _) =>
    2.10        Thm.add_def false true
    2.11 @@ -481,8 +480,7 @@
    2.12      val class_triv = Thm.class_triv def_thy class;
    2.13      val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
    2.14        def_thy
    2.15 -      |> Sign.add_path (Binding.name_of bconst)
    2.16 -      |> Sign.no_base_names
    2.17 +      |> Sign.sticky_prefix (Binding.name_of bconst)
    2.18        |> PureThy.note_thmss ""
    2.19          [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
    2.20           ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),