proper naming of simprocs according to actual target context;
afford pervasive declaration which makes results available with qualified name from outside;

--- a/src/Pure/Isar/proof_context.ML	Sat Mar 17 23:50:47 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 17 23:55:03 2012 +0100
@@ -141,6 +141,7 @@
     Context.generic -> Context.generic
   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
+  val target_naming_of: Context.generic -> Name_Space.naming
   val class_alias: binding -> class -> Proof.context -> Proof.context
   val type_alias: binding -> string -> Proof.context -> Proof.context
   val const_alias: binding -> string -> Proof.context -> Proof.context
@@ -992,6 +993,11 @@
 end;
 
 
+(* naming *)
+
+val target_naming_of = Context.cases Sign.naming_of naming_of;
+
+
 (* aliases *)
 
 fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;

--- a/src/Pure/simplifier.ML	Sat Mar 17 23:50:47 2012 +0100
+++ b/src/Pure/simplifier.ML	Sat Mar 17 23:55:03 2012 +0100
@@ -189,9 +189,8 @@
 
 fun gen_simproc prep {name = b, lhss, proc, identifier} lthy =
   let
-    val naming = Local_Theory.naming_of lthy;
     val simproc = make_simproc
-      {name = Name_Space.full_name naming b,
+      {name = Local_Theory.full_name lthy b,
        lhss =
         let
           val lhss' = prep lthy lhss;
@@ -201,8 +200,9 @@
        proc = proc,
        identifier = identifier};
   in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
       let
+        val naming = Proof_Context.target_naming_of context;
         val b' = Morphism.binding phi b;
         val simproc' = transform_simproc phi simproc;
       in