# HG changeset patch
# User haftmann
# Date 1226582349 -3600
# Node ID 677312de660823c4e34563f9df6d02937022405e
# Parent  8cbb7cfcfb5b53cc0898ed91f650824d926e48f6
consider prefixes for name bindings of simprocs (a first approximation)

diff -r 8cbb7cfcfb5b -r 677312de6608 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Nov 13 14:19:07 2008 +0100
+++ b/src/Pure/simplifier.ML	Thu Nov 13 14:19:09 2008 +0100
@@ -194,7 +194,9 @@
   in
     lthy |> LocalTheory.declaration (fn phi =>
       let
-        val name' = Name.name_of (Morphism.name phi (Name.binding name));
+        val binding = Morphism.name phi (Name.binding name);
+        val name' = NameSpace.implode
+          (map fst (Name.prefix_of binding) @ [Name.name_of binding]);
         val simproc' = morph_simproc phi simproc;
       in
         Simprocs.map (fn simprocs =>