# HG changeset patch
# User wenzelm
# Date 1441832487 -7200
# Node ID 6fced6d926be1c45b20cc05f59500d0fad5cda87
# Parent  497eb43a306496f857ce10cb0a9571a4c8f3d7a2
clarified declaration flags, like 'declaration' command;

diff -r 497eb43a3064 -r 6fced6d926be src/Pure/simplifier.ML
--- 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;