1.1 --- a/src/Pure/Isar/locale.ML	Thu Apr 26 12:00:01 2007 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Apr 26 12:00:05 2007 +0200
     1.3 @@ -1551,10 +1551,10 @@
     1.4  
     1.5  fun global_note_prefix_i kind (fully_qualified, prfx) args thy =
     1.6    thy
     1.7 -  |> Theory.qualified_names
     1.8 -  |> (if fully_qualified then Theory.sticky_prefix prfx else Theory.add_path prfx)
     1.9 +  |> Sign.qualified_names
    1.10 +  |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
    1.11    |> PureThy.note_thmss_i kind args
    1.12 -  ||> Theory.restore_naming thy;
    1.13 +  ||> Sign.restore_naming thy;
    1.14  
    1.15  fun local_note_prefix_i kind (fully_qualified, prfx) args ctxt =
    1.16    ctxt
    1.17 @@ -1726,8 +1726,8 @@
    1.18      val ([pred_def], defs_thy) =
    1.19        thy
    1.20        |> (if bodyT <> propT then I else
    1.21 -        Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
    1.22 -      |> Theory.add_consts_i [(bname, predT, NoSyn)]
    1.23 +        Sign.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
    1.24 +      |> Sign.add_consts_i [(bname, predT, NoSyn)]
    1.25        |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
    1.26      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
    1.27