consider prefixes for name bindings of simprocs (a first approximation)
authorhaftmann
Thu Nov 13 14:19:09 2008 +0100 (2008-11-13)
changeset 28738677312de6608
parent 28737 8cbb7cfcfb5b
child 28739 bbb5f83ce602
consider prefixes for name bindings of simprocs (a first approximation)
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/simplifier.ML	Thu Nov 13 14:19:07 2008 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Thu Nov 13 14:19:09 2008 +0100
     1.3 @@ -194,7 +194,9 @@
     1.4    in
     1.5      lthy |> LocalTheory.declaration (fn phi =>
     1.6        let
     1.7 -        val name' = Name.name_of (Morphism.name phi (Name.binding name));
     1.8 +        val binding = Morphism.name phi (Name.binding name);
     1.9 +        val name' = NameSpace.implode
    1.10 +          (map fst (Name.prefix_of binding) @ [Name.name_of binding]);
    1.11          val simproc' = morph_simproc phi simproc;
    1.12        in
    1.13          Simprocs.map (fn simprocs =>