dropped legacy naming code
authorhaftmann
Thu Nov 20 19:06:02 2008 +0100 (2008-11-20)
changeset 2886332e83a854e5e
parent 28862 53f13f763d4f
child 28864 d6fe93e3dcb9
dropped legacy naming code
src/Pure/name.ML
src/Pure/sign.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/name.ML	Thu Nov 20 14:55:28 2008 +0100
     1.2 +++ b/src/Pure/name.ML	Thu Nov 20 19:06:02 2008 +0100
     1.3 @@ -36,7 +36,6 @@
     1.4    val map_name: (string -> string) -> binding -> binding (*FIMXE legacy*)
     1.5    val qualified: string -> binding -> binding (*FIMXE legacy*)
     1.6    val display: binding -> string
     1.7 -  val namify: NameSpace.naming -> binding -> NameSpace.naming * string (*FIMXE legacy*)
     1.8  end;
     1.9  
    1.10  structure Name: NAME =
    1.11 @@ -167,14 +166,6 @@
    1.12      val pos = pos_of b;
    1.13    in f prefix (binding_pos (name, pos)) end;
    1.14  
    1.15 -fun namify naming b =
    1.16 -  let
    1.17 -    val (prefix, name) = dest_binding b
    1.18 -    fun mk_prefix (prfx, true) = sticky_prefix prfx
    1.19 -      | mk_prefix (prfx, false) = add_path prfx;
    1.20 -    val naming' = fold mk_prefix prefix naming;
    1.21 -  in (naming', full naming' name) end;
    1.22 -
    1.23  fun display b =
    1.24    let
    1.25      val (prefix, name) = dest_binding b
     2.1 --- a/src/Pure/sign.ML	Thu Nov 20 14:55:28 2008 +0100
     2.2 +++ b/src/Pure/sign.ML	Thu Nov 20 19:06:02 2008 +0100
     2.3 @@ -15,8 +15,6 @@
     2.4      consts: Consts.T}
     2.5    val naming_of: theory -> NameSpace.naming
     2.6    val base_name: string -> bstring
     2.7 -  val name_decl: (string * 'a -> theory -> 'b * theory)
     2.8 -    -> Name.binding * 'a -> theory -> (string * 'b) * theory
     2.9    val full_name: theory -> bstring -> string
    2.10    val full_binding: theory -> Name.binding -> string
    2.11    val full_name_path: theory -> string -> bstring -> string
    2.12 @@ -191,19 +189,6 @@
    2.13  val naming_of = #naming o rep_sg;
    2.14  val base_name = NameSpace.base;
    2.15  
    2.16 -fun name_decl decl (b, x) thy =
    2.17 -  let
    2.18 -    val naming = naming_of thy;
    2.19 -    val (naming', name) = Name.namify naming b;
    2.20 -  in
    2.21 -    thy
    2.22 -    |> map_naming (K naming')
    2.23 -    |> decl (Name.name_of b, x)
    2.24 -    |>> pair name
    2.25 -    ||> map_naming (K naming)
    2.26 -  end;
    2.27 -
    2.28 -val namify = Name.namify o naming_of;
    2.29  val full_name = NameSpace.full o naming_of;
    2.30  val full_binding = NameSpace.full_binding o naming_of;
    2.31  fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
     3.1 --- a/src/Pure/simplifier.ML	Thu Nov 20 14:55:28 2008 +0100
     3.2 +++ b/src/Pure/simplifier.ML	Thu Nov 20 19:06:02 2008 +0100
     3.3 @@ -194,12 +194,12 @@
     3.4    in
     3.5      lthy |> LocalTheory.declaration (fn phi =>
     3.6        let
     3.7 -        val (naming', name) = Name.namify naming (Morphism.name phi (Name.binding name));
     3.8 +        val b' = Morphism.name phi (Name.binding name);
     3.9          val simproc' = morph_simproc phi simproc;
    3.10        in
    3.11          Simprocs.map (fn simprocs =>
    3.12 -            NameSpace.extend_table naming' [(name, simproc')] simprocs
    3.13 -              handle Symtab.DUP dup => err_dup_simproc dup)
    3.14 +          NameSpace.table_declare naming (b', simproc') simprocs |> snd
    3.15 +            handle Symtab.DUP dup => err_dup_simproc dup)
    3.16          #> map_ss (fn ss => ss addsimprocs [simproc'])
    3.17        end)
    3.18    end;