src/Pure/simplifier.ML

         |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
        proc = proc,
        identifier = identifier}
       |> morph_simproc (LocalTheory.target_morphism lthy);
   in
-    lthy |> LocalTheory.declaration (fn phi =>
+    lthy |> LocalTheory.declaration false (fn phi =>
       let
         val b' = Morphism.binding phi b;
         val simproc' = morph_simproc phi simproc;
       in
         Simprocs.map (#2 o Name_Space.define true naming (b', simproc'))