clarified declaration flags, like 'declaration' command;

--- a/src/Pure/simplifier.ML	Wed Sep 09 21:51:44 2015 +0200
+++ b/src/Pure/simplifier.ML	Wed Sep 09 23:01:27 2015 +0200
@@ -137,7 +137,7 @@
       make_simproc lthy (Local_Theory.full_name lthy b)
         {lhss = prep lthy lhss, proc = proc, identifier = identifier};
   in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
       let
         val b' = Morphism.binding phi b;
         val simproc' = transform_simproc phi simproc;